Joachim Klein
|
07eb44539e
|
imported patch rewardcounter-CounterProduct.getStatesWithAccumulatedRewardInBoundConjunction.patch
|
7 years ago |
|
Joachim Klein
|
ef54f16e89
|
imported patch rewardcounter-IntegerBounds.isInBoundForConjunction.patch
|
7 years ago |
|
Joachim Klein
|
ea1a1ca21b
|
imported patch rewardcounter-IntegerBounds.getMaximalInterestingValueForConjunction.patch
|
7 years ago |
|
Joachim Klein
|
f1881a61e0
|
imported patch rewardcounter-TemporalBound.hasSameDomain.patch
|
7 years ago |
|
Joachim Klein
|
903eee7cbd
|
imported patch rewardcounter-groupBoundsByRewardStructure.patch
|
7 years ago |
|
Joachim Klein
|
0506cc412c
|
imported patch rewardcounter-TemporalBound.rewardStruct.patch
|
7 years ago |
|
Joachim Klein
|
bab19207a4
|
imported patch rewardcounter-MDPModelChecker.simple-path-formulas-with-bounds.patch
|
7 years ago |
|
Joachim Klein
|
ce1af01e42
|
imported patch rewardcounter-MDPCounterAndCounterTransformation.patch
|
7 years ago |
|
Joachim Klein
|
a012138134
|
imported patch rewardcounter-DTMCCounterTransformation.patch
|
7 years ago |
|
Joachim Klein
|
0dfbc3fc12
|
explicit: DTMCRewardCounterProduct
|
7 years ago |
|
Joachim Klein
|
a0fa61f265
|
imported patch rewardcounter-expression.getTemporalOperator.patch
|
7 years ago |
|
Joachim Klein
|
c47e6f7494
|
imported patch rewardcounter-IntegerBound.fromTemporalOperatorBound.patch
|
7 years ago |
|
Joachim Klein
|
53c679061c
|
imported patch rewardcounter-ReplaceBound.patch
|
7 years ago |
|
Joachim Klein
|
d769919086
|
imported patch rewardcounter-TemporalOperatorBounds-use-refresh.patch
|
7 years ago |
|
Joachim Klein
|
aeec397851
|
imported patch copyBoundsFrom-use-for-toUntil.patch
|
7 years ago |
|
Joachim Klein
|
f0bacc9ccc
|
imported patch copyBoundsFrom.patch
|
7 years ago |
|
Joachim Klein
|
32ada06833
|
imported patch FIX-temporal-bound-printing.patch
|
7 years ago |
|
Joachim Klein
|
6e033b5d65
|
imported patch rewardcounter-TemporalOperatorBounds-use.patch
|
7 years ago |
|
Joachim Klein
|
3fa0b761a5
|
imported patch rewardcounter-TemporalOperatorBounds.patch
|
7 years ago |
|
Joachim Klein
|
22ff99026f
|
imported patch rewardcounter-TemporalOperatorBound-use-refresh.patch
|
7 years ago |
|
Joachim Klein
|
fc07b9f9fb
|
imported patch rewardcounter-TemporalOperatorBound-use.patch
|
7 years ago |
|
Joachim Klein
|
2c4df3a20d
|
imported patch rewardcounter-TemporalOperatorBound.patch
|
7 years ago |
|
Joachim Klein
|
6cce20c5ed
|
imported patch prod-with-productstates-rely-on-product-for-soi.patch
|
7 years ago |
|
Joachim Klein
|
a08718e68b
|
imported patch rewardcounter-ProductWithProductStates.patch
|
7 years ago |
|
Joachim Klein
|
4d4faa7236
|
imported patch rewardcounter-MDPProductOperator.patch
|
7 years ago |
|
Joachim Klein
|
346a6e053e
|
explicit: +ProductOperator (generic)
|
7 years ago |
|
Joachim Klein
|
ba7e1c4c14
|
imported patch rewardcounter-ProductState-int.patch
|
7 years ago |
|
Joachim Klein
|
f2789fb0f5
|
explicit: +ProductState
|
7 years ago |
|
Joachim Klein
|
cfede9f44e
|
imported patch MET-ModelExpressionTransformationIdentity.patch
|
7 years ago |
|
Joachim Klein
|
bad808fd85
|
ModelExpressionTransformationNested
|
7 years ago |
|
Joachim Klein
|
bad132c250
|
Add ModelExpressionTransformation interface
|
7 years ago |
|
Joachim Klein
|
4ec20a4e34
|
imported patch symb-common-TemporaryJDDRefs.patch
|
7 years ago |
|
Joachim Klein
|
04a7e5ef56
|
imported patch common-REVERT-prodStatesList-explicit-LTLMC.patch
|
7 years ago |
|
Joachim Klein
|
5b0d6b0a6b
|
imported patch explicit-fairness-warning.patch
|
7 years ago |
|
Joachim Klein
|
764c2800ef
|
imported patch MT-states-of-interest.patch
|
7 years ago |
|
Joachim Klein
|
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 |
|
Joachim Klein
|
b50e56701b
|
(HOA path) LTL2DA: readHOA and fromExpressionHOA helpers
|
7 years ago |
|
Joachim Klein
|
bcded2e24f
|
(HOA path) PrismParser: PathSpecification supports LTL and HOA-style path specifications (parser refresh)
|
7 years ago |
|
Joachim Klein
|
cef6f8c35d
|
(HOA path) PrismParser: PathSpecification supports LTL and HOA-style path specifications
e.g. P=?[ HOA: { "automatonfile", "ap1" <- "label1", "ap2" <- "label2" } ]
|
7 years ago |
|
Joachim Klein
|
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 |
|
Joachim Klein
|
f6851caee7
|
(HOA path) PrismParser: support QuotedString (parser refresh)
|
7 years ago |
|
Joachim Klein
|
6b83df3d32
|
(HOA path) PrismParser: support QuotedString
REG_QUOTED_IDENT takes precedence over REG_QUOTED_STRING, therefore
QuotedString matches both.
|
7 years ago |
|
Joachim Klein
|
186da7e071
|
(HOA path) AST: QuotedString element
|
7 years ago |
|
Joachim Klein
|
badd6f924c
|
(HOA path) PrismParser: refactor double quoted identifiers (parser refresh)
|
7 years ago |
|
Joachim Klein
|
16c5442ab1
|
(HOA path) PrismParser: refactor double quoted identifiers
|
7 years ago |
|
Joachim Klein
|
ac02a22ae6
|
(HOA path) PrismPaths for resolving paths, e.g., relative to a model or properties file
|
7 years ago |
|
Joachim Klein
|
a58de4025a
|
(HOA path) PathUtil: Some static helper methods for dealing with paths
|
7 years ago |
|
Joachim Klein
|
7055482770
|
(HOA path) StateModelChecker (symbolic, explicit): Provide access to the ModulesFile / PropertiesFile stored in the model checker
|
7 years ago |
|
Joachim Klein
|
162e8e158a
|
(HOA path) Store ModulesFile / PropertiesFile location, if known
|
7 years ago |
|
Joachim Klein
|
0574b7973a
|
(HOA path) ModulesFile, PropertiesFile: optionally store location (path to file)
|
7 years ago |
