c576574ea0
imported patch rewardcounter-TemporalOperatorBound-use-refresh.patch
7 years ago
7345668608
imported patch rewardcounter-TemporalOperatorBound-use.patch
7 years ago
90d1864c7b
imported patch rewardcounter-TemporalOperatorBound.patch
7 years ago
65fc866101
imported patch prod-with-productstates-rely-on-product-for-soi.patch
7 years ago
2a6349a899
imported patch rewardcounter-ProductWithProductStates.patch
7 years ago
3a12bcbf20
imported patch rewardcounter-MDPProductOperator.patch
7 years ago
5282dbd9ce
explicit: +ProductOperator (generic)
7 years ago
ae9f852162
imported patch rewardcounter-ProductState-int.patch
7 years ago
f4ae67848b
explicit: +ProductState
7 years ago
423cd5a900
imported patch MET-ModelExpressionTransformationIdentity.patch
7 years ago
79149a48d1
ModelExpressionTransformationNested
7 years ago
e68696aeaf
Add ModelExpressionTransformation interface
7 years ago
1b30c76c0a
imported patch symb-common-TemporaryJDDRefs.patch
7 years ago
fb76b3c605
imported patch statevaluesmtbdd-print-flexible.patch
7 years ago
0e9113fcc6
imported patch remove-mtbdd-ssexport-restriction.patch
7 years ago
fbbb87c109
imported patch printall-symbolic.patch
7 years ago
04a1a9b735
imported patch common-REVERT-prodStatesList-explicit-LTLMC.patch
7 years ago
3aff21fcee
imported patch explicit-fairness-warning.patch
7 years ago
69b6f094e5
imported patch MT-states-of-interest.patch
7 years ago
d978661832
(HOA path) Add support in LTLModelCheckers (ex/sym) to support HOA path specifications
Additionally, protect multi-objective model checking and checkRewardCoSafeLTL against HOA path specifications.
Later on, we can add handling for that.
7 years ago
f7d3d182f8
(HOA path) LTL2DA: readHOA and fromExpressionHOA helpers
7 years ago
60f7cdec56
(HOA path) PrismParser: PathSpecification supports LTL and HOA-style path specifications (parser refresh)
7 years ago
8c1f67211a
(HOA path) PrismParser: PathSpecification supports LTL and HOA-style path specifications
e.g. P=?[ HOA: { "automatonfile", "ap1" <- "label1", "ap2" <- "label2" } ]
7 years ago
5e512c217f
(HOA path) ExpressionHOA for HOA-based path formula
* ExpressionHOA and visitor adaption
* Add Expression.isHOA to check for (negated) HOA expression
7 years ago
7af236f304
(HOA path) PrismParser: support QuotedString (parser refresh)
7 years ago
333d86e6d8
(HOA path) PrismParser: support QuotedString
REG_QUOTED_IDENT takes precedence over REG_QUOTED_STRING, therefore
QuotedString matches both.
7 years ago
f438c6f031
(HOA path) AST: QuotedString element
7 years ago
3fdc5e14b8
(HOA path) PrismParser: refactor double quoted identifiers (parser refresh)
7 years ago
adfe85b2fd
(HOA path) PrismParser: refactor double quoted identifiers
7 years ago
7e4b6180e6
(HOA path) PrismPaths for resolving paths, e.g., relative to a model or properties file
7 years ago
62196def2b
(HOA path) PathUtil: Some static helper methods for dealing with paths
7 years ago
185c9af2f7
(HOA path) StateModelChecker (symbolic, explicit): Provide access to the ModulesFile / PropertiesFile stored in the model checker
7 years ago
f3c143896b
(HOA path) Store ModulesFile / PropertiesFile location, if known
7 years ago
83a9996463
(HOA path) ModulesFile, PropertiesFile: optionally store location (path to file)
7 years ago
6dbf4c88e5
(HOA path) PropertiesFile: getters for ModelInfo and ModulesFile
7 years ago
dbeba66e9a
(HOA path) explicit MDP checker: allow Streett acceptance for LTL model checking
7 years ago
8a8f39d70a
imported patch prism-auto--property-list-file-with-arguments.patch
7 years ago
2f749bd92e
imported patch symb-common-symb-LTLMC-lift-reward.patch
7 years ago
c867d63120
imported patch iteration-method-jacobi-mdp-explicit.patch
7 years ago
4752262c26
JDD: add statisticsForDD(), printing CSV data about the number of nodes per level of a dd
7 years ago
61e29bd3e3
imported patch MET-ModelTransformationNested.patch
7 years ago
c6af64e0d9
common.BitSetAndQueue: Helper for iterating over a BitSet and a queue
7 years ago
47d5e573d6
Use reachability reward computation for complex state formulas
E.g., R=?[ F (a & A[F b])] was previously handled via co-safety, as
the operand of the F operator is not a proposition.
7 years ago
409ab5d199
add Expression.isReachWithStateFormula
isReach() is more restrictive, only allowing propositions as operand
of R=?[ F phi ], while we are also interested in the case where phi
as some complex state formula, potentially with nested operators, etc.
7 years ago
18d29bb612
imported patch Simplify-exact.patch
7 years ago
1a7e4100c7
imported patch catch-malformed-constants-in-results.patch
7 years ago
dd40cd018d
imported patch common-prismlog2csv.patch
7 years ago
c7d4d7e11d
sparse.cc: split_mdp_rec, protect against malformed MTBDD
7 years ago
4d672db58b
PrismSparse.exportMDP: sanity check
7 years ago
23c02e6b06
explicit engine: support -exportrows
7 years ago
Joachim Klein