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

59 Commits (881ecfef2f0e2b271e91418923c56a3280da1979)

Author SHA1 Message Date
Joachim Klein 881ecfef2f imported patch predecessor-LTLMC-use-backward.patch
7 years ago
Joachim Klein 3757da3fa0 imported patch rewardcounter-TemporalOperatorBounds-use.patch
7 years ago
Joachim Klein 04a1a9b735 imported patch common-REVERT-prodStatesList-explicit-LTLMC.patch
7 years ago
Joachim Klein d978661832 (HOA path) Add support in LTLModelCheckers (ex/sym) to support HOA path specifications
7 years ago
Joachim Klein 46d8ec3d8b explicit.LTLModelChecker: protect against int overflow if product state space can not be indexed by int
8 years ago
Joachim Klein 97074f5d58 Refactor explicit SCC computation, splitting SCCConsumer from SCCComputer.
9 years ago
Joachim Klein 9ef03e0c11 LTLModelCheckers: constructDFAForCosafetyRewardLTL
9 years ago
Joachim Klein 1071b362e7 explicit LTL, DTMC/MDP product: report product construction time, product statistics
9 years ago
Joachim Klein 204f972abb LTLModelChecker: add support for EC computations against Büchi acceptance
10 years ago
Joachim Klein e0bd1c22cb Cleanup DA-based simple path formula with bounds handling
10 years ago
Joachim Klein 9db978a12a switch to new way of obtaining acceptance type name
10 years ago
Joachim Klein 8af847bed5 explicit.LTLModelChecker: remove exception on constructor (never thrown) [Steffen Märcker]
10 years ago
Joachim Klein 2ea728c681 explicit.LTLModelChecker: accept any StateModelChecker (preparation for upcoming CTMC PCTL*-fix)
10 years ago
Joachim Klein 5d33639dd7 explicit.LTLModelChecker: Comment whitespace
10 years ago
Joachim Klein 298266c1cd explicit.LTLModelChecker: construct a VarList for the Model-DA product if the model had a varlist
10 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
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