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
ffa3809f35
imported patch tarjan-arraydeque.patch
7 years ago
179e177989
imported patch tarjan-deque.patch
7 years ago
4766932648
imported patch PrismCL-call-closedown-on-exit.patch
7 years ago
652271df38
imported patch PrismCL-protect-mainlog.patch
7 years ago
5d2aa3f977
imported patch PrismLog-ignoreClose.patch
7 years ago
0c972a8f83
Update manual.
5 years ago
eee992fd13
Version number (4.7).
5 years ago
5b35280d18
CHANGELOG.
5 years ago
7a6728a2d6
Add another simple POMDP example.
5 years ago
133a9eb406
Extend AccuracyFactory.valueAndAccuracyFromInterval to work for Inf.
5 years ago
11433e5121
Improve detection of infinite-valued states for POMDP expected reward.
Extend an existing test to cover this.
5 years ago
524dce617f
Add a check that clocks in POPTAs are observable.
5 years ago
c1ed8af218
Tidy up POMDP strategy export (via -exportadv).
Either exports in (MDP) .adv format (or belief model) .dot format,
depending on the extension of the filename provided.
5 years ago
e2ac8ee84e
More POMDP tests.
5 years ago
e594f2309b
POMDP computation performed for any (single) state, not just the initial one.
5 years ago
8a5b2f001d
POMDP refactoring: new Belief constructors.
5 years ago
90c7df8209
More refactoring in POMDP solution.
* Separate data structures for BeliefMDPState and POMDPStrategyModel
* Push reward construction/storage into the code for the belief MDP
* Factor out prob/reward backup operations into methods for re-use
* Store value function + backup using functional interfaces
* Collapse (now simpler) buildStrategyModel into one method
5 years ago
c8bde25ab4
Add support for checking probabilistic until for POMDPs.
5 years ago
2359f3e881
Some simple MDP-as-POMDP tests.
5 years ago
bc23e4e354
Refactor and improve POMDP approximate value iteration.
Grid points are only used for unknown (non-target) belief states.
5 years ago
0c6e283f5d
Refactor and improve construction of POMDP strategy model.
Allows action labels to be attached to the exported strategy dot file.
5 years ago
1bf07ddbcf
Tidying, refactoring and commenting in POMDP code.
5 years ago
969d7a4caf
Stricter check in POMDPSimple that actions match for observations.
It requires that the available actions are the same and appear in
the same order (in terms of choice indexing) in each equivalent state.
This always happens for PRISM models built via ConstructModel since
the model construction considers actions one by one in the same
order in each state (and actions must be unique for POMDPs).
5 years ago
0ec7c39525
Utility function NondetModel.getAvailableActions(s).
5 years ago
76a4b89855
Include observations in POMDP Dot model export.
5 years ago
d5e0fd4e66
Add convenience methods get(Un)ObservationAsState in PartiallyObservableModel.
5 years ago
2e5a4bfd56
Implement (extended) .tra file export for POMDPs.
5 years ago
ae0b960922
Enable simulation of POMDPs in the GUI.
5 years ago
Joachim Klein