Joachim Klein
46d0ac24dc
jhoafparser.jar (1.1.0)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10292 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
439d12108e
HOA in scripts readme.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10291 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
786797c467
CHANGELOG.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10290 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
187df335d1
Version numbering (4.3.beta)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10289 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
f9d02b349a
Fixes and improvements for LTL2RabinLibrary DRA generation.
Before, generating a DRA for L0 U L0 and bounded Until was broken.
The current code handles this and the other special case of L0 U !L0
correctly. Additionally, some small refactoring and comment improvements.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10288 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
0e3c380e5e
LTL2DA: Improve error handling.
In some cases, errors in LTL2RabinLibrary should be treated as
errors (when the formula contains temporal bounds), other times
we want to give jltl2dstar / the external LTL2DA tools another
try.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10287 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
fe95ece342
Deterministic automata: Better checking of atomic propositions
- Loosen check in LTL2DA for external automata, as the automata
having less APs than expected is fine
- Add generic checking in automata.DA, will catch problems no
matter the source of the automaton (jltl2dstar, HOA, LTL2RabinLibrary...)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10286 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
9fddd5c68a
Text for -help.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10282 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
ec7451ce5c
Text for -help.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10281 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
0328e60ac2
CHANGELOG.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10280 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
49a8d6ac70
CHANGELOG.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10279 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
5a672cf19b
CHANGELOG.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10278 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
127db9e354
set executable bit for hoa scripts
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10273 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
ff9f221bfd
rename HOA scripts to TDGRA for transition-based generalized-Rabin output
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10272 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
fc5464bee6
CHANGELOG.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10271 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
4c5d491717
Fix automata.DA.hasEdge(). Bug was introduced via the HOAF branch
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10270 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
88de17dd20
move the hoa- scripts to hoa subdirectory
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10269 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
6e60b93546
Maek hoa-library-for-prism executable
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10268 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
17b41eacc9
add hoa-library-for-prism script, for directly injecting HOA automata, useful for testing
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10267 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
7bd57c935f
HOAF2DA: Ensure that the automaton is actually complete.
As HOAF2DA will detect if there are multiple transitions with
the same label, we can just check that the number of transitions
is as expected.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10266 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
c714d88e6e
HOAF2DA: Limit atomic propositions to at most 30.
For more APs, the number of edges surpass what can
be stored in an int and we will get into trouble
with memory anyways.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10265 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
83ad513dc4
explicit.LTLModelChecker: catch missing edges in the DA for increased robustness
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10264 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
9f6777bed5
Regression tests: detect and warn about spaces in Error RESULT specifications.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10262 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
e73a7b2fb5
Undo regression test change: Error RESULT specifications cannot contains spaces (causes problems on specs with comments).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10261 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
30bec11226
Regression tests: Case-insensitive checks when comparing Error RESULT specifications.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10260 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
cdbc634b26
Regression testing: allow spaces in "Error" RESULT specifications.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10259 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
7c875e1929
Add "backwards" to -help.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10258 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
f927684aba
prism-auto: --help tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10257 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
952e550be7
prism-auto: Colour coding can be switched on/off with --colour switch (yes,no,auto).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10256 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
308ee00e64
prism-auto: Commenting
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10255 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
2228c6adda
TODO: HOAF2DA check for completeness
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10254 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
45317072c1
Some more comments for HOAF2DA
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10253 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
8aa9d24f5d
Colour code test results from prism-auto script.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10251 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
03b1d23e93
More library info.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10249 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
38335e4d6d
Add library version info.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10248 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
e85054f493
Rename jhoafparser jar.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10247 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
9aae97039c
PrismSettings: Switch PRISM_LTL2DA_SYNTAX to CHOICE_TYPE
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10246 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
7c65364af6
Update to version 2.5.5246 of JAS (and rename jar).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10245 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
8fed142e1e
Reinstate log4j - JAS uses it, apparently.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10244 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
1caa88764b
Remove (seemingly) unused log4j library.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10243 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
af7a1e7902
Bug fix (non-crucial) in explicit expected total cost.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10242 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
a14e6a39f9
CHANGELOG.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10241 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
3954b78eb1
Method name typo: JDD.AreInterecting -> JDD.AreIntersecting.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10236 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
4c877974dd
Code tidy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10235 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
4bb807cb8e
Code rearrange: move automata stuff to a separate "automata" package.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10234 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
a42e4108ee
More locale setting for outputting decimals in English.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10233 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
385d948194
Another locale setting for outputting decimals in English.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10232 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
2112f7b9b4
Fix javadoc target in main Makefile
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10229 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
bc29c96cbc
Cache the embedded DTMC inside CTMCSimple. This preserves the cached PredecessorRelation in the DTMC, allowing subsequent properties to be checked more efficiently. [from Joachim Klein]
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10225 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago