s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
2519 Commits
5 Branches
0 Tags
31 MiB
Tree: 9fddd5c68a
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '9fddd5c68a'
${ noResults }
Commit Graph

1885 Commits (9fddd5c68a5a33dc114939318dfc74c8cea54887)

Author SHA1 Message Date
Dave Parker 37b4284bfd DA can print to a PrismLog in either text or Dot format.
11 years ago
Dave Parker 8454511dad DA can print to a PrintStream or a PrismLog.
11 years ago
Dave Parker d2c08418db Add another simplification of DRAs - remove any state in a K_i set that does not occur in a non-trivial SCC of the DRA. This also allows more DRAs to be simplified to DFAs.
11 years ago
Dave Parker c17f92e172 Add LTS model type and expose underlying graph of a DA as an LTS.
11 years ago
Dave Parker e9afcf0419 Add default implementation of infoString() and infoStringTable() to ModelExplicit.
11 years ago
Dave Parker be834a8aff Align explicit SCComputer with symbolic one - it should not include trivial SCCs in the set computed; these should be stored separately.
11 years ago
Dave Parker a948079456 Fix comments in prism.SCCComputer to clarify that it computes non-trivial SCCs.
11 years ago
Dave Parker 98dcb3c803 Code tidy
11 years ago
Dave Parker 3fa59734a9 More use of PrismNotSupportedException.
11 years ago
Dave Parker 7352ad17b3 Small optimisation in LTL model checking: reduce number of propositions used in deterministic automaton by checking for negations.
11 years ago
Dave Parker b12953b937 Make use of the new PrismNotSupportedException.
11 years ago
Dave Parker 88928e8b89 New PrismNotSupportedException, to be throw when a model/prop/engine combination is not supported. Displays as UNSUPPORTED, not FAIL, in test mode. [from Joachim Klein]
11 years ago
Dave Parker fb7208d792 Improved "echo" (-e) functionality for prism-auto: displays more accurately what prism-auto would do, including test (-t) and log (-l) modes [from Joachim Klein].
11 years ago
Dave Parker 523d73a8ea Set locale for display of numerical values - otherwise, e.g. with LANG=de_DE.UTF-8, probabilities will be exported in the form 0,5 not 0.5 (reported by Joacim Klein).
11 years ago
Dave Parker 30c5001aaf Increase the default Java max memory (from to 512m to 2g) - should be ok these days.
11 years ago
Dave Parker c1681a04b2 Increase the default Java stack size - was consistently crashing on Tarjan SCC detection on a non-huge model (as reported by Steffen Marcker).
11 years ago
Dave Parker aa65fa1ea3 Fix documentation (-help xxx) about -exportmodel and -importmodel.
11 years ago
Dave Parker 079e9ea36a Typos.
11 years ago
Dave Parker 0b05a40aec Code tidy
11 years ago
Dave Parker a95d56bc20 Comment typo
11 years ago
Dave Parker 899806a26c Comment typos
11 years ago
Dave Parker 6c0ead6d2f Some useful additions to Pair utility class: implements Map.Entry and has a toString().
11 years ago
Dave Parker 6e1cf75a8e Some re-factoring of LTL model checking in the explicit engine.
11 years ago
Dave Parker 5e92fabe95 Comment typo.
11 years ago
Dave Parker c5b40f44d8 Code tidy.
11 years ago
Dave Parker 32ad9bbaae Code tidy.
11 years ago
Dave Parker 3e990e89e3 Some tidying/fixing in EC generation, including proper support in the explicit engine version for finding ECs that intersect with "accept".
11 years ago
Dave Parker 53cb310c7a Code tidy.
11 years ago
Dave Parker 60a30d7038 Comment typo.
11 years ago
Dave Parker bb6693f43d Allow comments to have no trailing new-line (e.g. when occurring at very end of file) - cannot see a good reason not to allow this.
11 years ago
Dave Parker 9729c78b3e Inefficiency in precomputatino routines in explicit engine (spotted by Steffen Marcker).
11 years ago
Dave Parker a744b15a7e Fix (again) computation of number of nondet choices for symbolic models (did not work for large number of nondet DD vars).
11 years ago
Dave Parker 5557db131f Remove debug output.
11 years ago
Dave Parker 56e323a2b4 Fix computation of number of nondet choices for symbolic models (did not work for large number of nondet DD vars).
11 years ago
Dave Parker 9fc29a3b25 Bug fix in symbolic model checking of co-safe properties (target was not ANDed with reachable states).
11 years ago
Dave Parker 38f0e001c2 Bugfix in PrismParser.isKeyword (leading to incorrect identification of bad identifiers in SBML/reactions to PRISM translation).
11 years ago
Dave Parker b8fc45249e Added sbml2prism script.
11 years ago
Dave Parker 6a1417c6f4 Bug fix in explicit engine CTMC until model checking (spotted by Chris Dehnert) (probably due to recent ProbModelChecker refactoring).
11 years ago
Dave Parker 3b8d17c352 Missing toString in AcceptanceReach (and output tweak in DA).
11 years ago
Dave Parker f7f4bf5f51 Model checkers: use DASimplify, allow AcceptanceReach in computations. [Joachim Klein]
11 years ago
Dave Parker ec4ddc4513 Add DASimplify. Currently supports simplifying DRA to DFA if the acceptance has a special form. [Joachim Klein]
11 years ago
Dave Parker c77bd235df Add AcceptanceReach, AcceptanceReachDD (for DFA style acceptance). [Joachim Klein]
11 years ago
Dave Parker d0384142bc LTLModelChecker: remove buildLStatesForRabinPair and buildKStatesForRabinPair, not needed anymore. [Joachim Klein]
11 years ago
Dave Parker 5b5bac7fe3 Adapt (symbolic) LTLModelChecker to support generic acceptance types for MDP. [Joachim Klein]
11 years ago
Dave Parker a16aeb57dc Adapt (symbolic) adapt LTLModelChecker to support generic acceptance types for DTMC. [Joachim Klein]
11 years ago
Dave Parker b6f3b2dce3 Adapt (explicit) LTLModelChecker to support generic acceptance types. [Joachim Klein]
11 years ago
Dave Parker f644011ba2 Refactor LTL-to-deterministic automaton generation, introduce LTL2DA and use LTL2RabinLibrary only for hard-coded and specially crafted DRA. [Joachim Klein]
11 years ago
Dave Parker 6ff3094b91 jltl2dstar: support generation of Rabin and Streett automata. [Joachim Klein]
11 years ago
Dave Parker 60ecccd9da New setting/switch: -pathviaautomata (all path formulas are handled via the LTL/DRA-engine), defaults to false. Honour in model checkers. [Joachim Klein]
11 years ago
Dave Parker 15a48d4fff LTLModelChecker.isSupportedLTLFormula(), for checking whether a path formula can be handled. [Joachim Klein]
11 years ago