Joachim Klein
7ddf026889
APSet: add asList() convenience method
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11276 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
c32cf2c94c
jltl2ba.APSet: source format, tidy up comments
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11275 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
32ffab4e94
jltl2ba.APSet: comments, add Iterable<APElement> elements() method
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11274 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Joachim Klein
5310be6b55
refactor SimpleLTL DAG check, remove common/PlainObjectReference.java
There's actually JDK library functionality for a hash map that
uses object identity instead of .equals(), making PlainObjectReference
unnecessary. Use IdentityHashMap instead.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11169 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
c11bec58ab
SimpleLTL: refactor/protect simplify(), check that formula graph is actually a tree
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10898 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
59f44c56ee
SimpleLTL: isTree() check to ensure that graph structure is tree, not DAG
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10897 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
e3b49ea35f
SimpleLTL: add toDot() output of the syntax tree / DAG
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10896 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
449b06ef8f
Add Jltl2baCmdLine command-line interface for LTL -> NBA functionality (for testing)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10534 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
6d3bfff9a6
jltl2ba.APElement: printing in LBTT / HOA format
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10525 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
5d3adc211c
jltl2ba.APSet: add print_hoa()
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10524 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
ca47143da5
SimpleLTL: add parsing functionality for LBT(T) formulas (prefix format)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10523 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
22bb6dea1c
Merge prism-hoaf branch back into trunk.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10231 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
73e2dfa94f
More jltl2ba and jltl2dstar bug fixes from Joachim Klein.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9355 bbc10eb1-c90d-0410-af57-cb519fbb1720
12 years ago
Dave Parker
f58712cd22
Next batch of LTL-related fixes from Joachim Klein (jltl2ba-fix-multiple-labels.patch, SimpleLTL-simplify-NEXT-AND-keep-order.patch, jltl2ba-fix-comments-for-release.patch, jltl2dstar-NBAAnalysis-dont-assume-NBA-is-disjoint.patch).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9153 bbc10eb1-c90d-0410-af57-cb519fbb1720
12 years ago
Dave Parker
c5e4ba4f73
Another LTL-to-automaton bugfix from Joachim Klein (jltl2ba-fix-simplify-bstates--trivial-sccs.patch).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9152 bbc10eb1-c90d-0410-af57-cb519fbb1720
12 years ago
Dave Parker
6594babe09
Another LTL-to-automaton bugfix from Joachim Klein (fix-bdfs.patch).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9151 bbc10eb1-c90d-0410-af57-cb519fbb1720
12 years ago
Dave Parker
78d3755e4e
A jltl2ba bug fix from Joachim Klein - fixes various previously reported LTL->DRA crashes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9109 bbc10eb1-c90d-0410-af57-cb519fbb1720
12 years ago
Dave Parker
07bf18a2f4
Fix makefiles with easier setup of classpath using * for jars.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4889 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Vojtech Forejt
e3f6e64e7a
package-info.java is ignored in makefiles
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4380 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
35f377ab3e
Improved documentation (JavaDoc mostly).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2436 bbc10eb1-c90d-0410-af57-cb519fbb1720
16 years ago
Dave Parker
0e7d9bd5b2
Carlos' latest updates to LTL code.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@802 bbc10eb1-c90d-0410-af57-cb519fbb1720
18 years ago
Dave Parker
5987dde299
Bug fixes in DRA libraries (Carlos).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@762 bbc10eb1-c90d-0410-af57-cb519fbb1720
19 years ago
Dave Parker
9d59912d3b
Working (but untidied) version of MDP LTL model checking.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@752 bbc10eb1-c90d-0410-af57-cb519fbb1720
19 years ago