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
cd5b101a10
imported patch JDDVars-merged.patch
7 years ago
6eabed4f09
SanityJDD: check for 'isVar', use in JDDVars.addVar
7 years ago
fbe3846ed4
imported patch JDD-SplitByValue.patch
7 years ago
2edbe1cf4c
imported patch sample-PrismUtils-bitsForEncoding.patch
7 years ago
5b1c8697f1
imported patch symb-dtmc-weights-support-negative-rewards.patch
7 years ago
2ed6c9486e
imported patch ex-dtmc-weights-support-negative-rewards.patch
7 years ago
38a64f0406
imported patch ex-dtmc-weights-MCRewardsPositive.patch
7 years ago
436f9a1c5a
imported patch ex-dtmc-weights-rewards-has-positive-negative.patch
7 years ago
2aa7d731ab
imported patch succ-it-from-trans-it.patch
7 years ago
87ab3ef9d1
Expression.isCoSafeLTLSyntactic: properly handle nesting and operator bounds
For determining syntactic co-safety, we are not interested in
the complex state formulas (e.g., with P, R, E, A, ... operators),
so we iterate without recursing into nested operators.
Furthermore, we currently don't support temporal operator bounds
for co-safety LTL formulas; check for those as well.
7 years ago
Joachim Klein