alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* README: Add descriptions for subdirectories of bench/, src/sanity,

Browse source 
and src/kripke.
This commit is contained in:
Alexandre Duret-Lutz 2010-01-24 10:37:07 +01:00
parent cbdb0feb68
commit 2919b64532
2 changed files with 50 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

5
ChangeLog
View file

@ -1,3 +1,8 @@
2010-01-24 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* README: Add descriptions for subdirectories of bench/, src/sanity,
and src/kripke.
2010-01-24 Guillaume Sadegh <sadegh@lrde.epita.fr> 2010-01-24 Guillaume Sadegh <sadegh@lrde.epita.fr>
* src/sanity/readme.test: A script to check whether all the * src/sanity/readme.test: A script to check whether all the

82
README
View file

@ -92,46 +92,52 @@ Layout of the source tree
Core directories Core directories
---------------- ----------------
src/ Sources for libspot. src/ Sources for libspot.
ltlast/ LTL abstract syntax tree (including nodes for ELTL). kripke/ Kripke Structure interface.
ltlenv/ LTL environments. ltlast/ LTL abstract syntax tree (including nodes for ELTL).
ltlparse/ Parser for LTL formulae. ltlenv/ LTL environments.
ltlvisit/ Visitors of LTL formulae. ltlparse/ Parser for LTL formulae.
ltltest/ Tests for ltlast/, ltlenv/, ltlparse/, and ltlvisit/. ltlvisit/ Visitors of LTL formulae.
misc/ Miscellaneous support files. ltltest/ Tests for ltlast/, ltlenv/, ltlparse/, and ltlvisit/.
tgba/ TGBA objects and cousins. misc/ Miscellaneous support files.
tgbaalgos/ Algorithms on TGBA. tgba/ TGBA objects and cousins.
gtec/ Couvreur's Emptiness-Check. tgbaalgos/ Algorithms on TGBA.
tgbaparse/ Parser for explicit TGBA. gtec/ Couvreur's Emptiness-Check.
tgbatest/ Tests for tgba/, tgbaalgos/, and tgbaparse/. tgbaparse/ Parser for explicit TGBA.
evtgba*/ Ignore these for now. tgbatest/ Tests for tgba/, tgbaalgos/, and tgbaparse/.
eltlparse/ Parser for ELTL formulae. evtgba*/ Ignore these for now.
eltltest/ Tests for ELTL nodes in ltlast/ and eltlparse/. eltlparse/ Parser for ELTL formulae.
saba/ SABA (State-labeled Alternating Büchi Automata) objects. eltltest/ Tests for ELTL nodes in ltlast/ and eltlparse/.
sabaalgos/ Algorithms on SABA. saba/ SABA (State-labeled Alternating Büchi Automata) objects.
sabatest/ Tests for saba/, sabaalgos/. sabaalgos/ Algorithms on SABA.
doc/ Documentation for libspot. sabatest/ Tests for saba/, sabaalgos/.
spot.html/ HTML reference manual. sanity/ Sanity tests for the whole project.
spot.latex/ Sources for the PDF manual. (Not distributed, can be rebuilt.) doc/ Documentation for libspot.
spotref.pdf PDF reference manual. spot.html/ HTML reference manual.
bench/ Benchmarks... spot.latex/ Sources for the PDF manual. (Not distributed, can be rebuilt.)
emptchk/ ... for emptiness-check algorithms, spotref.pdf PDF reference manual.
ltl2tgba/ ... for LTL-to-Büchi translation algorithms. bench/ Benchmarks for ...
wrap/ Wrappers for other languages. emptchk/ ... emptiness-check algorithms,
python/ Python bindings for Spot and BuDDy gspn-ssp/ ... various symmetry-based methods with GreatSPN,
tests/ Tests for these bindings ltl2tgba/ ... LTL-to-Büchi translation algorithms,
cgi/ Python-based CGI script (ltl-to-tgba translator) ltlcouter/ ... translation of a class of LTL formulae,
iface/ Interfaces to other libraries. scc-stats/ ... SCC statistics after translation of LTL formulae,
gspn/ GreatSPN interface. split-product/ ... parallelizing gain after splitting LTL automata.
examples/ Supporting models used by the test cases. wrap/ Wrappers for other languages.
nips/ NIPS interface (to use Promela models). python/ Python bindings for Spot and BuDDy
nipstest/ Tests for NIPS. tests/ Tests for these bindings
cgi/ Python-based CGI script (ltl-to-tgba translator)
iface/ Interfaces to other libraries.
gspn/ GreatSPN interface.
examples/ Supporting models used by the test cases.
nips/ NIPS interface (to use Promela models).
nipstest/ Tests for NIPS.
Third party software Third party software
-------------------- --------------------
buddy/ A patched version of BuDDy 2.3 (a BDD library). buddy/ A patched version of BuDDy 2.3 (a BDD library).
lbtt/ lbtt 1.2.0 (an LTL to Büchi automata test bench). lbtt/ lbtt 1.2.1 (an LTL to Büchi automata test bench).
iface/ Interfaces to other libraries. iface/ Interfaces to other libraries.
nips/ NIPS interface (to use Promela models). nips/ NIPS interface (to use Promela models).
nips_vm/ NIPS VM 1.2.7 (New Implementation of Promela Semantics nips_vm/ NIPS VM 1.2.7 (New Implementation of Promela Semantics
@ -151,5 +157,7 @@ End:
LocalWords: Python's BuDDy LBTT LTL Büchi lbtt gspn DIR GreatSPN Soheib Yann LocalWords: Python's BuDDy LBTT LTL Büchi lbtt gspn DIR GreatSPN Soheib Yann
LocalWords: Baarir Thierry Mieg CVS Università di Torino devel src libspot ac LocalWords: Baarir Thierry Mieg CVS Università di Torino devel src libspot ac
LocalWords: ltlast ltlenv ltlparse ltlvisit ltltest misc tgba TGBA tgbaalgos LocalWords: ltlast ltlenv ltlparse ltlvisit ltltest misc tgba TGBA tgbaalgos
LocalWords: gtec Tarjan tgbaparse tgbatest doc html PDF spotref pdf cgi LocalWords: gtec Tarjan tgbaparse tgbatest doc html PDF spotref pdf cgi ELTL
LocalWords: CGI ltl iface BDD Couvreur's evtgba emptchk LocalWords: CGI ltl iface BDD Couvreur's evtgba emptchk kripke Kripke saba vm
LocalWords: eltlparse eltltest SABA sabaalgos sabatest ssp ltlcouter scc SCC
LocalWords: Promela nipstest VM