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

117 Commits (f33dea0f43bb5ca39886bfbf2259f80b68ec1934)

Author SHA1 Message Date
Joachim Klein f33dea0f43 Interval iteration: Only print max finite value if it actually exists
8 years ago
Joachim Klein 09fc23a350 explicit.MDPModelChecker: prob0/1... methods take MDPGeneric instead of MDP as argument
8 years ago
Joachim Klein 194625a9c1 explicit.MDPModelChecker: for prob0e, generate strategy also for trivial case
8 years ago
Joachim Klein a14171b0b8 explicit model checkers: flag to silence log output during precomputations (prob0/1...)
8 years ago
Joachim Klein c2e86b5d2f (interval iteration) total reward computation is not supported yet, throw error message
9 years ago
Joachim Klein 80aec9a2fa cleanup some import warnings, artifacts of the recent set of refactorings...
9 years ago
Joachim Klein 65fd5cd795 (interval iteration, explicit) actually perform interval iteration using the explicit engine
9 years ago
Joachim Klein e97b72f6e6 explicit.MDPModelChecker: check for zero-reward ECs for Rmin=?[ F ] computations, use quotient model if necessary
9 years ago
Joachim Klein 1ce1446eb5 explicit.MDPModelChecker: support backward Gauss-Seidel during policy iteration
9 years ago
Joachim Klein 452d89e411 (explicit iteration refactoring) Expose topological value iterations via the -topological switch
9 years ago
Joachim Klein 12e377de4a (explicit iteration refactoring) DTMCModelChecker: use the new infrastructure for doing the numerical iteration computations.
9 years ago
Joachim Klein 7486c6d7ed For MDP model checking (explicit, symbolic), support -pmaxquotient option (computation in MEC quotient)
9 years ago
Joachim Klein 87675e828a explicit.MDPModelChecker: split numeric computation part of computeReachProbs into separate method
9 years ago
Joachim Klein 1fc8dfa9c4 (export-iterations) Explicit engine (DTMC/MDP): If enabled, export iterations to HTML file
9 years ago
Joachim Klein 37dff4f997 explicit: Use LTL2WDBA construction to obtain DFA for co-safe LTL reward computations
9 years ago
Joachim Klein c809c66ae9 explicit.MDPModelChecker: Rmax[ C ] (total reward) computation
9 years ago
Joachim Klein 0ee323ea6a explicit.MDPModelChecker: implement instantaneous reward computation (Rmax/min [I=x])
9 years ago
Joachim Klein 0667019a05 explicit: Make calls to StateModelChecker.loadLabelsFile static
9 years ago
Joachim Klein 55c0034a18 explicit model import: some more minor fixes to set correct initial states
9 years ago
Dave Parker 45466e9f1c Minor refactoring (for branch synching).
9 years ago
Dave Parker b76fe0e8b1 Add -exportprodvector switch, which exports solution vector over product model after checking LTL-based properties. Currently, supported in explicit engine, or symbolic engines where the result ends up being a vector of doubles (not an MTBDD).
10 years ago
Joachim Klein ae4b8c929e MDP model checking: allow Büchi acceptance
10 years ago
Dave Parker e85cceb572 Small tidies/fixes in explicit engine MDP strat generation.
10 years ago
Dave Parker bf76e587bc Small optimisation in explicit model checkers, when enlarging target for reachability. [from Steffen Marcker]
10 years ago
Dave Parker 1762db4d34 Bugfix in lifting rewards to product.
11 years ago
Dave Parker 21d663816a Push lifting of (explicit) reward structures into Reward classes.
11 years ago
Dave Parker 87bce928b1 Code tidy
11 years ago
Dave Parker fee3972b20 Bug fix in explicit co-ssafe reward computation.
11 years ago
Dave Parker 54bf906cc3 Missing -exporttarget case.
11 years ago
Dave Parker 957148215e Support (symbolic/explicit) for expected reward to satisfy a co-safe LTL formula.
11 years ago
Dave Parker 22bb6dea1c Merge prism-hoaf branch back into trunk.
11 years ago
Dave Parker 4da481df18 Remove debug output.
11 years ago
Dave Parker a6a371ee77 Remove debug output.
11 years ago
Dave Parker fae4eb38d7 Add support for -exporttarget to explicit engine.
11 years ago
Dave Parker 0984820760 Add support for -exportprodtrans and -exportprodstates switches to explicit engine.
11 years ago
Dave Parker d0f3e91387 Some code tidying (automatic mostly) for merging purposes.
11 years ago
Dave Parker 835e95a861 Don't print optimal strategy to screen when exporting it (explicit engine).
11 years ago
Dave Parker f7f4bf5f51 Model checkers: use DASimplify, allow AcceptanceReach in computations. [Joachim Klein]
11 years ago
Dave Parker b6f3b2dce3 Adapt (explicit) LTLModelChecker to support generic acceptance types. [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 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 e77138a79f computeRestrictedNext() for ProbModelChecker, NondetModelChecker, DTMCModelChecker and MDPModelChecker. [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 1f0382a0b6 LTL model checking optimisation - skip BSCC/EC detection if DRA is (syntactically) a DFA.
11 years ago
Dave Parker 50e8d24c02 Add -exportpropaut option (hidden) to export DRA(s) in textual form.
11 years ago
Dave Parker 0a5e0b6203 Additional checks in explicit MDP model checker: don't allow policy iteration methods to be use when 'known' values are passed in (from Joachim Klein).
11 years ago
Dave Parker 22e7009d7b Refactor explicit engine model checking of reward and steady state operators, as done recently for probabilistic stuff.
12 years ago