alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/src/tgbatest
History
Alexandre Duret-Lutz d401fadc65 neverparse: diagnose redefinition of state labels 
Reported by Joachim Klein.

* src/neverparse/neverclaimparse.yy: Store labels and the
location of their first definition in a global map to catch
redefinitions.
* src/tgbatest/neverclaimread.test: Test it.
* NEWS: Mention it.
2014-08-31 19:56:24 +02:00
..
.cvsignore more files to ignore 2004-06-22 22:58:09 +00:00
.gitignore Introduce some masked tgba. 2013-08-23 17:02:30 +02:00
babiak.test * src/tgbatest/babiak.test: Rewrite using ltlcross. 2013-01-10 18:42:36 +01:00
basimul.test ltlcross: add a --products=N option 2013-05-12 21:22:46 +02:00
bddprod.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
bitvect.cc bitvect: implement a dynamic bit-vector class. 2013-08-23 17:02:29 +02:00
bitvect.test bitvect: implement a dynamic bit-vector class. 2013-08-23 17:02:29 +02:00
complementation.cc Address several issues reported by cppcheck all over the place. 2012-12-24 13:14:33 +01:00
complementation.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
cycles.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
dbacomp.test tests: add some missing "set -e" 2013-11-22 02:13:57 +01:00
defs.in ltlcross: support short names 2013-11-22 02:13:57 +01:00
degendet.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
degenid.test degen: consider common outgoing acceptance only inside an SCC 2013-09-16 08:31:43 +02:00
degenlskip.test postproc: Add a degen-lskip option. 2014-04-07 18:21:06 +02:00
det.test bin: add support for reading formulas from CSV files. 2013-12-06 11:09:36 +01:00
dfs.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
dstar.test bitvect: fix block_count() on 0-sized bit-vectors 2014-01-24 09:25:48 +01:00
dupexp.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
eltl2tgba.test eltl2tgba: slight cleanup of the tests. 2013-01-17 14:06:31 +01:00
emptchk.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
emptchke.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
emptchkr.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
explicit.cc Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
explicit.test Arrange multops so that Boolean arguments come first. 2013-09-26 17:14:58 +02:00
explicit2.cc tgbaexplicit: fix state_is_accepting() 2012-10-21 00:02:07 +02:00
explicit2.test tgbaexplicit: fix state_is_accepting() 2012-10-21 00:02:07 +02:00
explicit3.cc Introduce some masked tgba. 2013-08-23 17:02:30 +02:00
explicit3.test Introduce some masked tgba. 2013-08-23 17:02:30 +02:00
explpro2.test Arrange multops so that Boolean arguments come first. 2013-09-26 17:14:58 +02:00
explpro3.test Arrange multops so that Boolean arguments come first. 2013-09-26 17:14:58 +02:00
explpro4.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
explprod.cc Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
explprod.test Arrange multops so that Boolean arguments come first. 2013-09-26 17:14:58 +02:00
intvcmp2.cc Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
intvcomp.cc Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
intvcomp.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
kv.test * src/tgbatest/kv.test: Fix the test comparison. 2012-10-12 22:09:16 +02:00
lbttparse.test lbtt: improve the LBTT output 2013-05-09 21:55:37 +02:00
ltl2dstar.test ltlcross: fix missing check for complement of negative automata 2014-08-31 19:56:24 +02:00
ltl2dstar2.test minimize_obligation: can complement the input TGBA if deterministic 2013-08-26 17:27:42 +02:00
ltl2neverclaim-lbtt.test tgbatest: Rewrite ltl2neverclaim using ltlcross. 2013-01-10 18:22:35 +01:00
ltl2neverclaim.test tgbatest: Rewrite ltl2neverclaim using ltlcross. 2013-01-10 18:22:35 +01:00
ltl2ta.test ltl2tgba_fm: Fix incorrect simplification of promises for M 2014-08-20 23:10:01 +02:00
ltl2ta2.test ltl2ta: fix a crash with --ta. 2014-04-07 18:21:10 +02:00
ltl2tgba.cc hoaf: first implementation of the HOA Format output. 2014-08-20 23:10:01 +02:00
ltl2tgba.test degen: consider common outgoing acceptance only inside an SCC 2013-09-16 08:31:43 +02:00
ltlcounter.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
ltlcross.test * src/tgbatest/ltlcross.test: More formulas from Joachim. 2014-08-21 23:16:39 +02:00
ltlcross2.test postproc: Add a degen-lskip option. 2014-04-07 18:21:06 +02:00
ltlcross3.test ltlcross: implement a --save-bogus=FILENAME option 2014-08-21 23:16:39 +02:00
ltlcross4.test Fix spurious failre with Pandas 0.13. 2014-02-06 01:33:17 +01:00
ltlcrossce.test tests: add some missing "set -e" 2013-11-22 02:13:57 +01:00
ltlprod.cc Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
ltlprod.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
Makefile.am ltl2ta: fix a crash with --ta. 2014-04-07 18:21:10 +02:00
mixprod.cc Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
mixprod.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
neverclaimread.test neverparse: diagnose redefinition of state labels 2014-08-31 19:56:24 +02:00
nondet.test bin: support multi-line CSV fields. 2013-12-06 13:45:55 +01:00
obligation.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
powerset.cc Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
randpsl.test ltl2tgba_fm: fix translation of !{f} as done last year for {f} 2014-08-21 23:16:39 +02:00
randtgba.cc Address several issues reported by cppcheck all over the place. 2012-12-24 13:14:33 +01:00
randtgba.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
readsat.cc sat: factor the creation of temporary files 2014-02-07 12:07:16 +01:00
readsat.test sat: generalize the code for reading the solution 2013-09-08 20:43:52 +02:00
readsave.test tgbaexplicit: speed up merge_transitions() 2012-10-19 17:53:08 +02:00
renault.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
satmin.test satmin: cleanup interfaces and minimization loops 2013-09-08 20:43:17 +02:00
satmin2.test * src/tgbatest/satmin2.test, src/tgbatest/Makefile.am: New test. 2014-02-08 20:31:49 +01:00
scc.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
sccsimpl.test Fix "BDD Error" in scc_filter(). 2013-06-19 21:21:16 +02:00
sim.test reachiter: fix the DFS, and add a version with on_stack() 2013-08-26 17:27:40 +02:00
sim2.test simulation: many fixes. 2013-04-09 15:05:55 +02:00
simdet.test Fix non determinism in the simulation. 2012-11-14 18:22:11 +01:00
spotlbtt.test Implement a favor_even_univ option in the rewriting rules. 2013-04-27 17:39:52 +02:00
spotlbtt2.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
taatgba.cc Fix Warning GCC 4.8 2013-04-27 18:33:24 +02:00
taatgba.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
tgbaread.cc Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
tgbaread.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
tripprod.cc Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
tripprod.test Arrange multops so that Boolean arguments come first. 2013-09-26 17:14:58 +02:00
wdba.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00
wdba2.test Upgrade GPL v2+ to GPL v3+. 2012-10-12 22:05:18 +02:00