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

707 Commits (a2e48a5c044e54e98a03ff28db22eda74e5d8492)

Author SHA1 Message Date
Joachim Klein 2c3d4a09e3 explicit.StateModelChecker: make loadLabelsFile static, use automatic close for BufferedReader
10 years ago
Dave Parker 45466e9f1c Minor refactoring (for branch synching).
10 years ago
Dave Parker 33d895baa1 Typo in last commit.
10 years ago
Dave Parker 9da9286c8c Remove some output to the log when processing filters (the number of satisfying states reported by this code can be wrong if the model checker optimises and only checks states satisfying the filter).
10 years ago
Dave Parker 4626d529a5 Code tidy
10 years ago
Dave Parker 09c5b11a74 Bug fix in ConstructModel - do not call attachLabels in justReach mode.
10 years ago
Joachim Klein 0e57919d0e explicit engine: Properly signal "not supported" for MDP total reward computations
10 years ago
Dave Parker bd9f2f255d Add slightly more efficient implementation of getChoiceAction for PRISM models.
10 years ago
Dave Parker 29b9286be3 Add some missing methods to DTMCFromMDPAndMDStrategy.
10 years ago
Dave Parker 95c3f7db43 Add a missing method in DTMCFromMDPAndMDStrategy.
10 years ago
Dave Parker d309f8c748 Comment fix.
10 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).
11 years ago
Joachim Klein ae4b8c929e MDP model checking: allow Büchi acceptance
11 years ago
Joachim Klein 204f972abb LTLModelChecker: add support for EC computations against Büchi acceptance
11 years ago
Joachim Klein e0bd1c22cb Cleanup DA-based simple path formula with bounds handling
11 years ago
Joachim Klein 9db978a12a switch to new way of obtaining acceptance type name
11 years ago
Joachim Klein 8af847bed5 explicit.LTLModelChecker: remove exception on constructor (never thrown) [Steffen Märcker]
11 years ago
Joachim Klein 432d017bbf explicit.StateValues: add createFromIntegerArray (analogue to createFromBitSet, createFromDoubleArray)
11 years ago
Joachim Klein 578d33e7f1 explicit.LTSNBAProduct: take atomic propositions of NBA into account
11 years ago
Joachim Klein ca2a9e0caa explicit: non-probabilistic LTL via E[ ltl ] and A[ ltl ]
11 years ago
Joachim Klein 071d26d603 explicit.LTSNBAProduct: Construct and store the product of a model and an NBA as a LTS
11 years ago
Joachim Klein 432c569691 explicit.LTSExplicit: Storage for an LTS
11 years ago
Joachim Klein 8889db5a2a explicit.CTMCModelChecker: reject LTL with time bounds
11 years ago
Joachim Klein 8be0e36cbe explicit.PredecessorRelation: consistently use getPre()
11 years ago
Joachim Klein 38617a9184 explicit: add support for CTL model checking
11 years ago
Joachim Klein 802abccbce explicit.StateValues: add complement() method (for boolean vectors)
11 years ago
Joachim Klein 45b837567b explicit.CTMCModelChecker: fix handling of PCTL* subformulas
11 years ago
Joachim Klein 4dd6a008d4 explicit.StateModelChecker: handleMaximalStateFormulas by recursive checking and attaching labels to the model
11 years ago
Joachim Klein 2ea728c681 explicit.LTLModelChecker: accept any StateModelChecker (preparation for upcoming CTMC PCTL*-fix)
11 years ago
Joachim Klein 650e519e2d DTMCEmbeddedSimple: pass through label methods to underlying CTMC
11 years ago
Joachim Klein 19dd97cdd4 explicit: add ModelExplicit.addUniqueLabel() to help with attaching generated labels to a model
11 years ago
Joachim Klein 19a1111491 explicit: add Model.hasLabel() method
11 years ago
Dave Parker b6828a7045 Remove unused "techLog" from Prism object and other classes.
11 years ago
Dave Parker a025ae2e07 Add model checking of R[C] operator for CTMCs.
11 years ago
Dave Parker 4c13267ded Add test methods for special cases in ExpressionLabels.
11 years ago
Dave Parker de50d8d145 Small update to previous commit: display filter size *before* possibly optimising it.
11 years ago
Dave Parker 031a14e778 Small optimisation when model checking filters: Reduce set of filter states to the first state if filter is "first". [from Steffen Marcker]
11 years ago
Dave Parker 66ea7475a7 Optimisation when dealing with filters: perform cardinality check for "state" filters earlier. [from Steffen Marcker]
11 years ago
Dave Parker eda5876325 Minor refactoring, ahead of upcoming patches. [from Steffen Marcker]
11 years ago
Dave Parker 0f2bbbc7b6 Add some (syntactic) reward info to the ModelInfo interface and use this where possible in explicit model checking. Can now use ModulesFileModelGenerator for reward property model checking. Also push constant info from ModelGenerator up to ModelInfo.
11 years ago
Dave Parker c8a894cae2 Auto-format.
11 years ago
Dave Parker d4a86d5c2d Remove ModelExplorer interface and replace with ModelGenerator.
11 years ago
Dave Parker 589b0b1a17 Remove defunct field from ConstructModel.
11 years ago
Dave Parker 0e01288705 Improve explicit.ConstructModel: generalise to use new ModelGenerator interface (not just ModulesFiles via the simulator) and tidy up the settings within the class.
11 years ago
Dave Parker 9ce7e6441b Push containsUnboundedVariables methof from VarList up into ModulesFile.
11 years ago
Dave Parker 4aea86b501 Comment clarifications.
11 years ago
Dave Parker e85cceb572 Small tidies/fixes in explicit engine MDP strat generation.
11 years ago
Dave Parker fb37c9a22d Slight refactoring of strategy storage in explicit engine (to match PRISM-games).
11 years ago
Dave Parker 8597f0e71b Extend previous commit (reachability enlarging target) to STPG model checking.
11 years ago
Dave Parker bf76e587bc Small optimisation in explicit model checkers, when enlarging target for reachability. [from Steffen Marcker]
11 years ago