/dports/math/spot/spot-2.10.2/tests/python/ |
H A D | satmin.py | 35 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1) 50 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2) 79 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1) 94 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2) 126 state_based=True, max_states=5, sat_incr=1) 130 state_based=True, max_states=5, sat_incr=1, 135 state_based=True, max_states=5, sat_incr=1, 140 state_based=True, max_states=5, sat_incr=1, 145 state_based=True, max_states=5, sat_incr=1, 193 colored=True, sat_incr=1) [all …]
|
H A D | satmin.ipynb | 2393 …"Using `sat_incr=1`, we encode the problem of finding an equivalent automaton with $n$ states, and… 2655 "spot.sat_minimize(large, acc='co-Buchi', sat_incr=1, state_based=True, display_log=True)" 2662 …going to state $n-i$ are forbidden. This variant is enabled by option `sat_incr=2`. As in the pr… 2915 "spot.sat_minimize(large, acc='co-Buchi', sat_incr=2, state_based=True, display_log=True)" 3185 …"aut, log = spot.sat_minimize(large, acc='co-Buchi', sat_incr=2, state_based=True, return_log=True…
|
/dports/math/py-spot/spot-2.10.2/tests/python/ |
H A D | satmin.py | 35 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=1) 50 min1 = spot.sat_minimize(aut, acc='Rabin 1', sat_incr=2) 79 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=1) 94 min2 = spot.sat_minimize(aut, acc='Streett 2', sat_incr=2) 126 state_based=True, max_states=5, sat_incr=1) 130 state_based=True, max_states=5, sat_incr=1, 135 state_based=True, max_states=5, sat_incr=1, 140 state_based=True, max_states=5, sat_incr=1, 145 state_based=True, max_states=5, sat_incr=1, 193 colored=True, sat_incr=1) [all …]
|
H A D | satmin.ipynb | 2393 …"Using `sat_incr=1`, we encode the problem of finding an equivalent automaton with $n$ states, and… 2655 "spot.sat_minimize(large, acc='co-Buchi', sat_incr=1, state_based=True, display_log=True)" 2662 …going to state $n-i$ are forbidden. This variant is enabled by option `sat_incr=2`. As in the pr… 2915 "spot.sat_minimize(large, acc='co-Buchi', sat_incr=2, state_based=True, display_log=True)" 3185 …"aut, log = spot.sat_minimize(large, acc='co-Buchi', sat_incr=2, state_based=True, return_log=True…
|
/dports/math/spot/spot-2.10.2/spot/twaalgos/ |
H A D | dtwasat.cc | 1386 int sat_incr = om.get("sat-incr", 0); in sat_minimize() local 1398 if (sat_incr == 1 && !sat_incr_steps) // Assume in sat_minimize() 1400 else if (sat_incr == 2 && !sat_incr_steps) // Incremental in sat_minimize() 1503 else if (sat_incr == 1) in sat_minimize() 1507 else if (sat_incr == 2) in sat_minimize() 1521 else if (sat_incr == 1) in sat_minimize() 1525 else if (sat_incr == 2) in sat_minimize()
|
/dports/math/py-spot/spot-2.10.2/spot/twaalgos/ |
H A D | dtwasat.cc | 1386 int sat_incr = om.get("sat-incr", 0); in sat_minimize() local 1398 if (sat_incr == 1 && !sat_incr_steps) // Assume in sat_minimize() 1400 else if (sat_incr == 2 && !sat_incr_steps) // Incremental in sat_minimize() 1503 else if (sat_incr == 1) in sat_minimize() 1507 else if (sat_incr == 2) in sat_minimize() 1521 else if (sat_incr == 1) in sat_minimize() 1525 else if (sat_incr == 2) in sat_minimize()
|
/dports/math/spot/spot-2.10.2/python/spot/ |
H A D | __init__.py | 1251 sat_incr=0, sat_incr_steps=0, argument 1272 if sat_incr: 1273 args += ',sat-incr=' + str(sat_incr)
|
/dports/math/py-spot/spot-2.10.2/python/spot/ |
H A D | __init__.py | 1251 sat_incr=0, sat_incr_steps=0, argument 1272 if sat_incr: 1273 args += ',sat-incr=' + str(sat_incr)
|