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

44 Commits (ad238d314caf181b97cb780e24fad0130fb9f390)

Author SHA1 Message Date
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
11 years ago
Dave Parker 590ae94e9f Refactor explicit engine product construction.
11 years ago
Dave Parker 80c8dcd09d Refactor explicit engine product construction.
11 years ago
Dave Parker 9e434ad9ea Merge in explicit engine detection of end components for Streett acceptance. [from Joachim Klein]
11 years ago
Joachim Klein fe95ece342 Deterministic automata: Better checking of atomic propositions
11 years ago
Joachim Klein 83ad513dc4 explicit.LTLModelChecker: catch missing edges in the DA for increased robustness
11 years ago
Dave Parker 4bb807cb8e Code rearrange: move automata stuff to a separate "automata" package.
11 years ago
Dave Parker 22bb6dea1c Merge prism-hoaf branch back into trunk.
11 years ago
Dave Parker 0984820760 Add support for -exportprodtrans and -exportprodstates switches to explicit engine.
11 years ago
Dave Parker b4f05f3cd0 Add possibility to specify type to -exportpropaut switch (dot or txt), e.g. -exportpropaut:dot dra.dot.
11 years ago
Dave Parker 98dcb3c803 Code tidy
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 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 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 15a48d4fff LTLModelChecker.isSupportedLTLFormula(), for checking whether a path formula can be handled. [Joachim Klein]
11 years ago
Dave Parker 9ad8e8165e LTL2RabinLibrary and model checkers: support automata based constructions for temporal bounds for simple path formulas. Now, the constantValues from the model checker have to be passed to LTL2RabinLibrary to allow resolving constants in the bounds. [Joachim Klein]
11 years ago
Dave Parker a18d74e5b6 provide LTLModelChecker.constructProductMDP(MDP mdp, Expression ltl), encapsulating DA generation and product construction. [Joachim Klein]
11 years ago
Dave Parker e3ce1e85ee provide LTLModelChecker.constructProductMC(DTMC dtmc, Expression ltl), encapsulating DA generation and product construction. [Joachim Klein]
11 years ago
Dave Parker ab81007716 Lift stored labels and statelist to the product model. [Joachim Klein]
11 years ago
Dave Parker 36991a899a Refactor LTL product construction in explicit engine. [Joachim Klein]
11 years ago
Dave Parker c00ffea7d8 Refactor: switch from prism.DRA<BitSet> to prism.DA<BitSet, AcceptanceRabin>. Changes access to the Rabin pairs. [Joachim Klein]
11 years ago
Dave Parker 7e6f8e8cf6 Revert recent DFA optimizations to allow for acceptance type refactoring. Functionality will be later readded using AcceptanceReach. [Joachim Klein]
11 years ago
Dave Parker 0b8223c685 Explicit engine: Add BitSet statesOfInterest parameter to the various checkExpression... methods [Joachim Klein].
11 years ago
Dave Parker 797f9494b2 Explicit engine: Add BitSet statesOfInterest parameter to the various checkExpression... methods [Joachim Klein].
11 years ago
Dave Parker 9f4a6dba5f LTL explicit engine bug fix (from Joachim Klein).
11 years ago
Dave Parker 1f0382a0b6 LTL model checking optimisation - skip BSCC/EC detection if DRA is (syntactically) a DFA.
11 years ago
Dave Parker 7f10ec8b60 Bug in explicit engine LTL model checking (happens when there are multiple APs in the formula and ordering is different in the DRA). Reported by Manfred Jaeger.
12 years ago
Dave Parker 3ddadc504e Comment typo
12 years ago
Dave Parker 99a9c85a96 Fixes/tidies of explicit LTL model checking (mostly from Joachim Klein): DRA products correctly include all initial states, and probabilities are ampped back correctly.
12 years ago
Dave Parker 6f5213111b Fix explicit MDP model checking (EC computation was incorrect) + some refactoring.
13 years ago
Dave Parker 39f12fefe2 Refactoring in explicit EC computation (but MDP model checking stil not working).
13 years ago
Dave Parker bce5d3f3be MDP-LTL model checking for explicit (still needs fixing) + correction to DTMC-DRA product construction.
13 years ago
Dave Parker 54b9aea80b Tidy up of symbolic/explicit SCC/EC computer classes, incl. integration of PrismComponent interface + knock-on effects.
13 years ago
Dave Parker 4c23a25e45 Comments + minor refactoring.
13 years ago
Dave Parker 2b6a966076 DRA-DTMC product code works for any type of DTMC, not just DTMCSimple.
13 years ago
Dave Parker 115953fd5e Optimise DRA-DTMC product construction.
13 years ago
Dave Parker 67476e300f Minor tweaks to new DTMC-LTL code.
13 years ago
Dave Parker 9e52b90863 Patch in DTMC-LTL model checking for explicit engine (from prism-games-bruni).
13 years ago