alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/tests/python
History
Alexandre Duret-Lutz 9ab4b840fd simulation: do not depend on bdd numbers for ordering classes 
Fixes #262 again.  Reported by Maximilien Colange.

* spot/twaalgos/simulation.cc: Use state numbers to order classes, not
their signatures.  The problem was that even if two simulation of the
same automaton assign the same signature, the BDD identifier used for
that signature might be different, and therefore the ordering obtained
by using BDDs as keys in a map can be different.  A side-effect of
this change is that the order of states in automata produced by
simulation-based reduction may change; many tests had to be updated.
* tests/core/ltl2tgba.test: Add a new test case based on Maximilien's
report.
* tests/core/complement.test, tests/core/det.test,
tests/core/parseaut.test, tests/core/prodor.test, tests/core/scc.test,
tests/python/atva16-fig2a.ipynb, tests/python/automata.ipynb,
tests/python/decompose.ipynb, tests/python/decompose_scc.py,
tests/python/highlighting.ipynb, tests/python/piperead.ipynb,
tests/python/sccinfo.py, tests/python/simstate.py,
tests/python/testingaut.ipynb, tests/python/word.ipynb: Update
test case for new order of states.
2017-06-02 14:10:34 +02:00
..
.gitignore Merge the core and python tests in the tests/ directory 2016-01-04 16:02:30 +01:00
_altscc.ipynb dot: fix printing of alternating automata 2017-05-31 17:55:15 +02:00
_aux.ipynb python: report dot errors 2016-02-16 14:34:57 +01:00
acc_cond.ipynb mark_t: sets() no longer returns a vector 2017-04-20 14:06:57 +02:00
accparse.ipynb Merge the core and python tests in the tests/ directory 2016-01-04 16:02:30 +01:00
accparse2.py acc: add a maybe_accepting() method 2017-05-31 17:18:03 +02:00
alarm.py parsetl: change the interface to return a parsed_formula 2016-02-17 20:31:58 +01:00
alternating.py introduce spot::split_edges() 2017-05-05 22:25:12 +02:00
alternation.ipynb twa_graph: add a merge_univ_dests() method 2016-12-29 12:57:53 +01:00
atva16-fig2a.ipynb simulation: do not depend on bdd numbers for ordering classes 2017-06-02 14:10:34 +02:00
atva16-fig2b.ipynb python: add the examples from the ATVA'16 paper 2016-06-17 14:18:48 +02:00
automata-io.ipynb dot: add option C(COLOR) 2016-02-05 19:26:38 +01:00
automata.ipynb simulation: do not depend on bdd numbers for ordering classes 2017-06-02 14:10:34 +02:00
bdditer.py python: add bindings for bdd_to_formula() 2017-03-08 15:39:08 +01:00
bddnqueen.py Merge the core and python tests in the tests/ directory 2016-01-04 16:02:30 +01:00
bugdet.py dtwa_complement: deprecated, use dualize() instead. 2017-04-07 17:15:38 +02:00
declenv.py parsetl: improve coverage 2017-03-15 14:23:19 +01:00
decompose.ipynb simulation: do not depend on bdd numbers for ordering classes 2017-06-02 14:10:34 +02:00
decompose_scc.py simulation: do not depend on bdd numbers for ordering classes 2017-06-02 14:10:34 +02:00
dualize.py implement dualize to complement automatons 2017-04-07 17:15:38 +02:00
formulas.ipynb python: render the M&P hierarchy in SVG 2017-01-18 20:58:20 +01:00
gen.ipynb gen: hide ks_cobuchi(), introduce aut_pattern() 2017-04-28 13:32:03 +02:00
gen.py gen: set more properties in automata 2017-04-28 13:32:48 +02:00
highlighting.ipynb simulation: do not depend on bdd numbers for ordering classes 2017-06-02 14:10:34 +02:00
implies.py Merge the core and python tests in the tests/ directory 2016-01-04 16:02:30 +01:00
interdep.py parsetl: change the interface to return a parsed_formula 2016-02-17 20:31:58 +01:00
ipnbdoctest.py python: update some incorrect or obsolete code 2017-03-29 20:04:08 +02:00
langmap.py langmap: adjust to only color non-unique languages 2017-01-17 21:58:03 +01:00
ltl2tgba.py parsetl: change the interface to return a parsed_formula 2016-02-17 20:31:58 +01:00
ltl2tgba.test Merge the core and python tests in the tests/ directory 2016-01-04 16:02:30 +01:00
ltlf.py from_ltlf: new LTL transformation. 2016-11-05 22:59:02 +01:00
ltlparse.py python: update some incorrect or obsolete code 2017-03-29 20:04:08 +02:00
ltlsimple.py Merge the core and python tests in the tests/ directory 2016-01-04 16:02:30 +01:00
ltsmin-dve.ipynb emptiness: allow twa_run::as_twa to preserve names 2017-02-04 10:02:23 +01:00
ltsmin-pml.ipynb adjust tests to SpinS 1.1 2016-06-22 21:26:35 +02:00
minato.py Merge the core and python tests in the tests/ directory 2016-01-04 16:02:30 +01:00
misc-ec.py emptiness checks: replace assert-preconditions by exceptions 2017-03-10 14:36:22 +01:00
optionmap.py Merge the core and python tests in the tests/ directory 2016-01-04 16:02:30 +01:00
origstate.py Degeneralization keeps track of levels. 2017-05-31 13:28:42 +02:00
otfcrash.py cleanup ltsmin bindings 2016-02-16 19:08:28 +01:00
parsetgba.py Merge the core and python tests in the tests/ directory 2016-01-04 16:02:30 +01:00
piperead.ipynb simulation: do not depend on bdd numbers for ordering classes 2017-06-02 14:10:34 +02:00
prodexpt.py typos: dictionnary -> dictionary 2017-03-08 16:10:47 +01:00
product.ipynb rename is_deterministic to is_universal 2017-03-27 19:34:10 +02:00
randaut.ipynb Merge the core and python tests in the tests/ directory 2016-01-04 16:02:30 +01:00
randgen.py Merge the core and python tests in the tests/ directory 2016-01-04 16:02:30 +01:00
randltl.ipynb Merge the core and python tests in the tests/ directory 2016-01-04 16:02:30 +01:00
relabel.py Merge the core and python tests in the tests/ directory 2016-01-04 16:02:30 +01:00
remfin.py dtwa_complement: deprecated, use dualize() instead. 2017-04-07 17:15:38 +02:00
rs_like.py rs_like: fix bug to accept Fin | Fin , Inf & Inf 2017-05-29 11:45:02 +02:00
satmin.py twaalgos: Set 'dicho' algo as default for SAT-based minimization 2017-01-06 19:53:21 +01:00
sccfilter.py scc_filter: preserve state names and highlighted states 2016-11-11 15:21:17 +01:00
sccinfo.py simulation: do not depend on bdd numbers for ordering classes 2017-06-02 14:10:34 +02:00
setacc.py twa: do not set prop_state_acc in set_acceptance 2016-11-11 15:20:56 +01:00
setxor.py Merge the core and python tests in the tests/ directory 2016-01-04 16:02:30 +01:00
simstate.py simulation: do not depend on bdd numbers for ordering classes 2017-06-02 14:10:34 +02:00
sum.py dtwa_complement: deprecated, use dualize() instead. 2017-04-07 17:15:38 +02:00
testingaut.ipynb simulation: do not depend on bdd numbers for ordering classes 2017-06-02 14:10:34 +02:00
trival.py trival: new class for tri-valued logic 2016-01-13 17:57:54 +01:00
twagraph.py twa_graph: fix purge_unreachable_states on alternating automata 2017-03-29 10:08:23 +02:00
word.ipynb simulation: do not depend on bdd numbers for ordering classes 2017-06-02 14:10:34 +02:00