Sebastian Junges
|
f77e8b2dc2
|
added a minimal test for makecanonic
|
4 years ago |
|
Sebastian Junges
|
9e2bc9b341
|
testing for writing to global vars from action-labelled models
|
4 years ago |
|
Sebastian Junges
|
271fdb0607
|
minimalistic test cases for building POMDPs added
|
4 years ago |
|
Sebastian Junges
|
922d6f6572
|
export of compressed states to json with negative values fixed
|
4 years ago |
|
Sebastian Junges
|
f910288aea
|
global command indices may not be from 0 to N, so we have to check for highest command index explicitly
|
4 years ago |
|
Sebastian Junges
|
f43cb6a798
|
fix testfile
|
4 years ago |
|
Sebastian Junges
|
b9bd9e2fd4
|
parser test for nary predicates
|
4 years ago |
|
Sebastian Junges
|
a4e8d9ea11
|
post-merge fix to when substituting predicates and unbounded integers
|
4 years ago |
|
Sebastian Junges
|
cf63ea6767
|
eliminate nonstandard predicates early on
|
4 years ago |
|
Sebastian Junges
|
bbbe178572
|
Cleaning and support for linux platforms
|
4 years ago |
|
Sebastian Junges
|
85b676ff57
|
better output
|
4 years ago |
|
Sebastian Junges
|
65ba87dbd0
|
removed debug output
|
4 years ago |
|
Sebastian Junges
|
1218991e6a
|
can switch off producing schedulers in the instantiation model checker
|
4 years ago |
Tim Quatmann
|
bdd89d87b2
|
Prism next state generator now deals with unbounded integer variables.
|
4 years ago |
|
Tim Quatmann
|
1fe0254f5d
|
DdPrismModelBuilder now errors in case it has a program with unbounded integer variables as input
|
4 years ago |
|
Tim Quatmann
|
9f1c540f05
|
Counterexamples:making minimal label set generator aware of unbounded integer variables
|
4 years ago |
|
Tim Quatmann
|
171ff270e0
|
Prism to Jani conversion now supports unbounded integer variables
|
4 years ago |
|
Tim Quatmann
|
8f9ff95531
|
Added Test cases for parsing/processing prism programs that use unbounded integer variables
|
4 years ago |
|
Tim Quatmann
|
5c2b9c503c
|
prism/Program: Integer variables can now have no lower and/or upper bound.
|
4 years ago |
|
Tim Quatmann
|
aa5bb9cb7d
|
PrismParser: Parsing unbounded integer variables
|
4 years ago |
|
Tim Quatmann
|
871efc0d8c
|
Fixed TerminalStatesGetter with multi-bounded formulae.
|
4 years ago |
Daniel Basgöze
|
c3859ec021
|
Add merge operation to RelevantEvents
|
4 years ago |
|
Daniel Basgöze
|
8bccb7ffa1
|
Fix const correctness in RelevantEvents
|
4 years ago |
|
Daniel Basgöze
|
7cd2394078
|
Make RelevantEvents independent of std::vector
Instead use a flexible iterator based api
|
4 years ago |
|
Tim Quatmann
|
d5c6a509a2
|
JaniNextStateGenerator: Fixed evaluation of terminal states using expressions over transient variables
|
4 years ago |
|
Tim Quatmann
|
95d53e444b
|
Fixed an issue with jani::VariablSet using different kinds of variable names when adding and deleting variables.
|
4 years ago |
|
Tim Quatmann
|
66e6938d20
|
added a few clarifying comments in JaniNextStateGenerator
|
4 years ago |
|
Sebastian Junges
|
e3251c7500
|
reset reward from last action upon reset
|
4 years ago |
|
Sebastian Junges
|
a7f9a6e4c6
|
use state rewards (upon entry)
|
4 years ago |
|
Tim Quatmann
|
168b5fabd6
|
Silenced several warnings
|
4 years ago |
|
Tim Quatmann
|
45a7db8222
|
LpMinMaxLinearEquationSolver: Fixed an issue when using glpk occurring when the lower bound of a variable matches the upper bound. Also revamped retrieving of lower/upper bounds.
|
4 years ago |
|
Tim Quatmann
|
e59918668e
|
AbstractEquationSolver: Added more convenient getters for the most appropriate lower/upper bound of a given variable
|
4 years ago |
Matthias Volk
|
6df0efcd3e
|
Set result correctly for reachability rewards in MdpInstantiationChecker
|
4 years ago |
|
Tim Quatmann
|
eaff65ef27
|
LinearCoefficientVisitor: Fixed translation of division expressions.
|
4 years ago |
|
Sebastian Junges
|
5d45514af2
|
avoid parsing jani after creating model - fix in lvalue to allow this
|
4 years ago |
|
Sebastian Junges
|
3355b21b72
|
add timing info to storm-pomdp
|
4 years ago |
|
Sebastian Junges
|
d6ab421cb7
|
add belief-support-mdp generator
|
4 years ago |
|
Sebastian Junges
|
3c58b5b2f7
|
case split for MDPs actually checks for MDPs
|
4 years ago |
|
Sebastian Junges
|
08f928456c
|
fix guard for code that considers transient assignments to also consider only transient assignments
|
4 years ago |
|
Sebastian Junges
|
6b6f44100e
|
allow building parametric models of the form s --p-->, s--q-->
|
4 years ago |
|
Sebastian Junges
|
7beb999219
|
label unlabelled commands
|
4 years ago |
|
Sebastian Junges
|
71f60e812c
|
more precise analysis of whether commands will synchronize
|
4 years ago |
|
Sebastian Junges
|
c4187b03eb
|
fixed error messages
|
4 years ago |
|
Sebastian Junges
|
a5842e4a61
|
nasty bug where some sync action indices where not reflected in one of the data structures
|
4 years ago |
|
Sebastian Junges
|
7daa5e2ab7
|
fixed error message
|
4 years ago |
|
Matthias Volk
|
9fea07542a
|
Fixed warning
|
4 years ago |
|
Matthias Volk
|
c9841b71a0
|
Const reference for splittingThreshold
|
4 years ago |
Jip Spel
|
8d17a0362d
|
Fix extremal value computation
|
4 years ago |
|
Daniel Basgöze
|
0ed64b6257
|
Add == and != ops to RelevantEvents
and simplify constructor of RelevantEvents
|
4 years ago |
|
Daniel Basgöze
|
7a2b060afc
|
Remove allowDCForRelevant from RelevantEvents
|
4 years ago |
