DFTL

CMakeLists.txt

@@ -97,6 +97,7 @@ target_sources(oink
     src/zlkpp.cpp
     src/ptl.cpp
     src/dtl.cpp
+    src/dftl.cpp
     ${OINK_HDRS}
 )
 
@@ -178,6 +179,10 @@ if(CMAKE_CURRENT_SOURCE_DIR STREQUAL CMAKE_SOURCE_DIR)
         add_executable(counter_qpt src/tools/counter_qpt.cpp)
         set_target_props(counter_qpt)
 
+        add_executable(counter_odftl src/tools/counter_odftl.cpp)
+        set_target_props(counter_odftl)
+        target_link_libraries(counter_odftl oink)
+
         add_executable(tc src/tools/tc.cpp)
         set_target_props(tc)
         target_link_libraries(tc oink)
@@ -225,6 +230,8 @@ if(CMAKE_CURRENT_SOURCE_DIR STREQUAL CMAKE_SOURCE_DIR)
         add_test(NAME TestSolverSPPTL COMMAND test_solvers ${CMAKE_CURRENT_SOURCE_DIR}/tests --spptl)
         add_test(NAME TestSolverDTL COMMAND test_solvers ${CMAKE_CURRENT_SOURCE_DIR}/tests --dtl)
         add_test(NAME TestSolverIDTL COMMAND test_solvers ${CMAKE_CURRENT_SOURCE_DIR}/tests --idtl)
+        add_test(NAME TestSolverDFTL COMMAND test_solvers ${CMAKE_CURRENT_SOURCE_DIR}/tests --dftl)
+        add_test(NAME TestSolverODFTL COMMAND test_solvers ${CMAKE_CURRENT_SOURCE_DIR}/tests --odftl)
         # test ZLK variations
         add_test(NAME TestSolverZLKseq COMMAND test_solvers ${CMAKE_CURRENT_SOURCE_DIR}/tests --zlk -w -1)
         add_test(NAME TestSolverZLKpar COMMAND test_solvers ${CMAKE_CURRENT_SOURCE_DIR}/tests --zlk -w 0)

README.md

@@ -46,6 +46,8 @@ PTL             | Progressive Tangle Learning (research variant)
 SPPTL           | Single-player Progressive Tangle Learning (research variant)
 DTL             | Distance Tangle Learning (research variant based on 'good path length')
 IDTL            | Interleaved Distance Tangle Learning (interleaved variant of DTL)
+DFTL            | Distraction-Free Tangle Learning (two-player variant)
+ODFTL           | One-player Distraction-Free Tangle Learning
 
 ### Fixpoint algorithms
 
@@ -195,6 +197,7 @@ counter\_rob   | SCC version of counter\_core.
 counter\_dtl   | Counterexample to the DTL solver
 counter\_ortl  | Counterexample to the ORTL solver
 counter\_symsi | Counterexample of Matthew Maat to (standard) symmetric strategy improvement
+counter\_dftl  | Counterexample to the DFTL solver
 tc             | Two binary counters generator (game family that is an exponential lower bound for many algorithms). See also Tom van Dijk (2019) [A Parity Game Tale of Two Counters](https://doi.org/10.4204/EPTCS.305.8). In: GandALF 2019.
 tc+            | TC modified to defeat the RTL solver
 
@@ -212,7 +215,7 @@ The two binary counters game family appears to be a quasi-polynomial lower bound
 * The progress measures variations SSPM, QPT
 
 Some algorithms can solve the two binary counters games in polynomial time:
-* The tangle learning algorithms RTL, ORTL, PTL, SPPTL, DTL, IDTL
+* The tangle learning algorithms RTL, ORTL, PTL, SPPTL, DTL, IDTL, DFTL, PDFTL
 * The strategy improvement algorithm PSI
 * Unsure: the BSSPM and BQPT algorithms