Home
last modified time | relevance | path

Searched refs:sat_incr (Results 1 – 8 of 8) sorted by relevance

/dports/math/spot/spot-2.10.2/tests/python/
H A Dsatmin.py35 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 Dsatmin.ipynb2393 …"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 Dsatmin.py35 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 Dsatmin.ipynb2393 …"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 Ddtwasat.cc1386 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 Ddtwasat.cc1386 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__.py1251 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__.py1251 sat_incr=0, sat_incr_steps=0, argument
1272 if sat_incr:
1273 args += ',sat-incr=' + str(sat_incr)