cfede9f44e
imported patch MET-ModelExpressionTransformationIdentity.patch
7 years ago
bad808fd85
ModelExpressionTransformationNested
7 years ago
bad132c250
Add ModelExpressionTransformation interface
7 years ago
4ec20a4e34
imported patch symb-common-TemporaryJDDRefs.patch
7 years ago
04a7e5ef56
imported patch common-REVERT-prodStatesList-explicit-LTLMC.patch
7 years ago
5b0d6b0a6b
imported patch explicit-fairness-warning.patch
7 years ago
764c2800ef
imported patch MT-states-of-interest.patch
7 years ago
a79bc54188
(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
b50e56701b
(HOA path) LTL2DA: readHOA and fromExpressionHOA helpers
7 years ago
bcded2e24f
(HOA path) PrismParser: PathSpecification supports LTL and HOA-style path specifications (parser refresh)
7 years ago
cef6f8c35d
(HOA path) PrismParser: PathSpecification supports LTL and HOA-style path specifications
e.g. P=?[ HOA: { "automatonfile", "ap1" <- "label1", "ap2" <- "label2" } ]
7 years ago
2a2d7d64c9
(HOA path) ExpressionHOA for HOA-based path formula
* ExpressionHOA and visitor adaption
* Add Expression.isHOA to check for (negated) HOA expression
7 years ago
f6851caee7
(HOA path) PrismParser: support QuotedString (parser refresh)
7 years ago
6b83df3d32
(HOA path) PrismParser: support QuotedString
REG_QUOTED_IDENT takes precedence over REG_QUOTED_STRING, therefore
QuotedString matches both.
7 years ago
186da7e071
(HOA path) AST: QuotedString element
7 years ago
badd6f924c
(HOA path) PrismParser: refactor double quoted identifiers (parser refresh)
7 years ago
16c5442ab1
(HOA path) PrismParser: refactor double quoted identifiers
7 years ago
ac02a22ae6
(HOA path) PrismPaths for resolving paths, e.g., relative to a model or properties file
7 years ago
a58de4025a
(HOA path) PathUtil: Some static helper methods for dealing with paths
7 years ago
7055482770
(HOA path) StateModelChecker (symbolic, explicit): Provide access to the ModulesFile / PropertiesFile stored in the model checker
7 years ago
162e8e158a
(HOA path) Store ModulesFile / PropertiesFile location, if known
7 years ago
0574b7973a
(HOA path) ModulesFile, PropertiesFile: optionally store location (path to file)
7 years ago
de07381f87
(HOA path) PropertiesFile: getters for ModelInfo and ModulesFile
7 years ago
e7759bfe37
(HOA path) explicit MDP checker: allow Streett acceptance for LTL model checking
7 years ago
75930b200d
imported patch prism-auto--property-list-file-with-arguments.patch
7 years ago
2fe3302c7f
imported patch symb-common-symb-LTLMC-lift-reward.patch
7 years ago
a418d42793
imported patch iteration-method-jacobi-mdp-explicit.patch
7 years ago
32ac7e1f07
JDD: add statisticsForDD(), printing CSV data about the number of nodes per level of a dd
7 years ago
35e1bd4071
imported patch MET-ModelTransformationNested.patch
7 years ago
c021a8050a
common.BitSetAndQueue: Helper for iterating over a BitSet and a queue
7 years ago
e5fd6b4f73
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
f4dab093cb
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
4f24c71e7e
imported patch Simplify-exact.patch
7 years ago
32b870eba9
imported patch catch-malformed-constants-in-results.patch
7 years ago
dd450d0ca6
imported patch common-prismlog2csv.patch
7 years ago
d85ba48d2c
sparse.cc: split_mdp_rec, protect against malformed MTBDD
7 years ago
3266756b20
imported patch JDDVars-merged.patch
7 years ago
bec320dc60
SanityJDD: check for 'isVar', use in JDDVars.addVar
7 years ago
aaefc225db
imported patch JDD-SplitByValue.patch
7 years ago
916c7e3f90
imported patch sample-PrismUtils-bitsForEncoding.patch
7 years ago
8179f24fbd
imported patch symb-dtmc-weights-support-negative-rewards.patch
7 years ago
b2b785cb28
imported patch ex-dtmc-weights-support-negative-rewards.patch
7 years ago
cdb00e1c36
imported patch ex-dtmc-weights-MCRewardsPositive.patch
7 years ago
4789f61827
imported patch ex-dtmc-weights-rewards-has-positive-negative.patch
7 years ago
e20f66e8bd
imported patch succ-it-from-trans-it.patch
7 years ago
2e6659a177
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
30153de9cc
ExpressionTraverseNonNested: handle strategy, CTL operators as well
We don't want to recurse into the strategy or CTL operators.
Refactor a bit to keep the boilerplate code for each visit() method down.
7 years ago
b0a2923635
imported patch sccmethodex-setting.patch
7 years ago
fbb89e74e9
imported patch tmp-tarjan-iterative-2.patch
7 years ago
4f73085483
imported patch tarjan-lowlink-index-array.patch
7 years ago
Joachim Klein