Stefan Pranger
5562007866
introduced PostScheduler
this allows for different choice mappings per state, in the sense of
'what should I schedule if another scheduler has already picked a
different action'
4 years ago
Stefan Pranger
4b2e7e020f
restructured shield creation
construct is no longer a pure virtual function because of different
return types for different shields. Ctor is still protected so no issues
here.
Added computeRowGroupSizes method
4 years ago
Stefan Pranger
3decad58b9
introduced shield export
Still needs a proper naming convention for the shields to be unique
4 years ago
Stefan Pranger
f605ec28e3
fixed bug in safety shield creation
4 years ago
Stefan Pranger
caf855e1a4
added first version of pre safety shield
4 years ago
Stefan Pranger
d1a39e48fe
removed unused template instantiations
4 years ago
Stefan Pranger
750efef3b5
made shielding printout prettier
4 years ago
Stefan Pranger
0f7555a8e0
fetch choice values from until vi computation
- added an SMGModelCheckingHelperReturnType
4 years ago
Stefan Pranger
8943b01df5
added shield handling header
4 years ago
Stefan Pranger
359f20b17d
init first shield implementation
4 years ago
Stefan Pranger
c9d5e2959a
let MDP helper return type store choiceValues
4 years ago
Stefan Pranger
0c619c097c
WIP: init shielding for SMGs
4 years ago
Stefan Pranger
5051b9f9f7
fixed typo
4 years ago
Stefan Pranger
dccb9e5f8b
changed some debug output
4 years ago
Stefan Pranger
72baec5ec1
substituteFormula now respects shieldExpression
4 years ago
Stefan Pranger
a3da5642f1
removed unused member of checkTask
4 years ago
Stefan Pranger
d9db7d57b3
parsing ShieldExpression into shared_ptr
4 years ago
Stefan Pranger
102b26b933
CheckTask may now hold info about shielding query
4 years ago
Stefan Pranger
d4d3c0d9ea
Jani Props may now hold info about shielding query
4 years ago
Stefan Pranger
00479b4877
added printout for shielding queries
4 years ago
Stefan Pranger
283f4ea6a2
added toString method for ShieldExpression
4 years ago
Stefan Pranger
66a8e472e3
added ostream for ShieldExpression
4 years ago
Stefan Pranger
fa47742a14
added checks for multiplicative factor parsing
4 years ago
Stefan Pranger
f6b341168d
added formula parser grammar for shields
4 years ago
Stefan Pranger
16fafbcfcc
properties now hold information about shield query
4 years ago
Stefan Pranger
5a2657346b
added shield expression class
4 years ago
6f39d431a3
Github Actions: only run doxygen and deploy on master branch of original
repository (and not on forks or pull requests).
4 years ago
Stefan Pranger
7ef70401ed
Merge pull request 'boundedGlobally' ( #19 ) from next_formulae into main
Reviewed-on: https://git.pranger.xyz/TEMPEST/tempest-devel/pulls/19
4 years ago
Lukas Posch
027ed523cd
added constrainedChoiceValues for boundedGloballyFormulas
4 years ago
168b5fabd6
Silenced several warnings
4 years ago
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
e59918668e
AbstractEquationSolver: Added more convenient getters for the most appropriate lower/upper bound of a given variable
4 years ago
Lukas Posch
59c5aeadea
changed message for boundedGloballyFormula
4 years ago
Lukas Posch
f6829dd109
clean up BoundedGloballyGameViHelper
4 years ago
Lukas Posch
0fd952c6f7
removed b
4 years ago
Lukas Posch
bcd67c63f7
removed "...Reachability" from GameViHelper and BoundedGloballyGameViHelper
4 years ago
Lukas Posch
5e040553a6
changed error message
4 years ago
Lukas Posch
0ea549864f
fixed assert for using lowerBounds
4 years ago
Lukas Posch
02bc7f3f69
added assert for using lowerBounds
4 years ago
6df0efcd3e
Set result correctly for reachability rewards in MdpInstantiationChecker
4 years ago
Lukas Posch
64861445fe
bug fix bounded globally
4 years ago
eaff65ef27
LinearCoefficientVisitor: Fixed translation of division expressions.
4 years ago
5d45514af2
avoid parsing jani after creating model - fix in lvalue to allow this
4 years ago
3355b21b72
add timing info to storm-pomdp
4 years ago
d6ab421cb7
add belief-support-mdp generator
4 years ago
3c58b5b2f7
case split for MDPs actually checks for MDPs
4 years ago
08f928456c
fix guard for code that considers transient assignments to also consider only transient assignments
4 years ago
6b6f44100e
allow building parametric models of the form s --p-->, s--q-->
4 years ago
Lukas Posch
8df4a99770
small changes, but did not fix the bug
4 years ago
Lukas Posch
489d8a5fd2
added bounds to model checker and parse it for probability calculation of bounded globally formulas
4 years ago
Matthias Volk
Tim Quatmann
Sebastian Junges