Dave Parker
ce6ffdcc13
Default format type for DA.print methods.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10755 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
3464a921ad
First version of Nailgun support built directly into PRISM. Adding switch -ng when running prism will instead start a Nailgun server ready to run PRISM instances, and running ngprism runs PRISM as a Nailgun client.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10588 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
b4a1fc0b79
Code tidy (auto-format).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10567 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
d791bce62f
Add some more options to LTL2DA program
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10543 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
6e5a62eb42
Add some more options to LTL2DA program
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10542 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
7f6c068e8b
Add a simple command-line test program (LBT->HOA) to LTL2DA.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10541 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
ad238d314c
Allow -exportpropaut to export DA in HOA format, e.g.: prism dice.pm -pf "P=?[X X d=6]" -exportpropaut:hoa da.hoa
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10537 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
c79a27b218
HOAF2DA: add main() method to provide command-line interface for testing deterministic HOA parsing.
Reads a deterministic HOA automaton, stores in internal PRISM DA format and prints it back out.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10536 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
b1863bb528
automata.DA: printHOA()
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10533 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Joachim Klein
2fe9a4d994
More gracefully handle deterministic automata in HOAF2DA
If the HOA automaton has multiple edges to the same state, do not throw an error.
Additionally, better error reporting.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10300 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
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
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
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
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