d769919086
imported patch rewardcounter-TemporalOperatorBounds-use-refresh.patch
7 years ago
aeec397851
imported patch copyBoundsFrom-use-for-toUntil.patch
7 years ago
f0bacc9ccc
imported patch copyBoundsFrom.patch
7 years ago
32ada06833
imported patch FIX-temporal-bound-printing.patch
7 years ago
6e033b5d65
imported patch rewardcounter-TemporalOperatorBounds-use.patch
7 years ago
3fa0b761a5
imported patch rewardcounter-TemporalOperatorBounds.patch
7 years ago
22ff99026f
imported patch rewardcounter-TemporalOperatorBound-use-refresh.patch
7 years ago
fc07b9f9fb
imported patch rewardcounter-TemporalOperatorBound-use.patch
7 years ago
2c4df3a20d
imported patch rewardcounter-TemporalOperatorBound.patch
7 years ago
6cce20c5ed
imported patch prod-with-productstates-rely-on-product-for-soi.patch
7 years ago
a08718e68b
imported patch rewardcounter-ProductWithProductStates.patch
7 years ago
4d4faa7236
imported patch rewardcounter-MDPProductOperator.patch
7 years ago
346a6e053e
explicit: +ProductOperator (generic)
7 years ago
ba7e1c4c14
imported patch rewardcounter-ProductState-int.patch
7 years ago
f2789fb0f5
explicit: +ProductState
7 years ago
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
Joachim Klein