 Stefan Pranger
|
505c830d42
|
set optdir overrides from multiplier env
|
4 years ago |
|
Stefan Pranger
|
c7d7be8b83
|
nondetTs may also be gameNondetTs in LraViHelper
|
4 years ago |
|
Stefan Pranger
|
de385b0527
|
added method for lra game transition type
also added the according template class constructions.
|
4 years ago |
|
Stefan Pranger
|
4c7968b4cf
|
added and finalized NondetGamehelper methods
This still needs some better documentation for the introduced class
methods.
Also removed some debug printing.
|
4 years ago |
|
Stefan Pranger
|
ea90c1ac7d
|
added and finalized methods for rpatlMC
|
4 years ago |
|
Stefan Pranger
|
f72f83f23e
|
computeLongRunAverageValues is now virtual
in SparseInfiniteHorizonHelper, since
SparseNondeterministicGameInfiniteHorizonHelper needs to overwrite it.
|
4 years ago |
|
Stefan Pranger
|
b61d947057
|
parse coalition operator and set row group optdirs
|
4 years ago |
|
Stefan Pranger
|
9ef1ec5f50
|
added opt dir override bitvector to multiplier
This is mainly used by the SMG model checker to override row group
optimization directions.
|
4 years ago |
|
Stefan Pranger
|
c11c49d22b
|
store tuples of player name and index
Store this instead of only the index. Needed for easier parsing of the
rpatl formulas (prism allows player indices and names!)
|
4 years ago |
|
Stefan Pranger
|
af38bc3b4d
|
added transition type for games to LraViHelper
|
4 years ago |
|
Stefan Pranger
|
0a689d232e
|
init helper for games
|
4 years ago |
|
Stefan Pranger
|
19839036af
|
AbstractMC passes game formula to the rpatl MC
|
4 years ago |
|
Stefan Pranger
|
0a65e4aa7b
|
verification now handles SMGs
|
4 years ago |
|
Stefan Pranger
|
21af5c5d6a
|
handle model description ostream case for SMGs
|
4 years ago |
|
Stefan Pranger
|
b599ff5c7e
|
added sparse MC templates for SMGs
|
4 years ago |
|
Stefan Pranger
|
d1a0299bd0
|
buildMatrices handles playerIndices via reference
|
4 years ago |
|
Stefan Pranger
|
e88a83d9aa
|
engine now checks smg models
|
4 years ago |
|
Stefan Pranger
|
a299504361
|
added smg rpatl model checker
|
4 years ago |
|
Stefan Pranger
|
d939ebe375
|
smg model now stores the player action indices
|
4 years ago |
|
Stefan Pranger
|
353b98ec88
|
rpatl extends prctl
|
4 years ago |
|
Stefan Pranger
|
1470d65586
|
gameForumlas now gather referenced variables
|
4 years ago |
|
Stefan Pranger
|
6cea196953
|
rpatl smg formulas now accept operatorFormulas
|
4 years ago |
|
Stefan Pranger
|
a9868fd501
|
refactor Coalition to use boost variant
|
4 years ago |
|
Stefan Pranger
|
84bcfef24e
|
removed print from CloneVisitor
|
4 years ago |
|
Stefan Pranger
|
2fb1f36fda
|
Merge branch 'keep-module-index-map-in-parsing' into game_formula_parsing
|
4 years ago |
|
Stefan Pranger
|
53ac9a3873
|
fixed typo in arg list of GameFormula
|
4 years ago |
|
Stefan Pranger
|
376e4756db
|
added Coalition default ctor
|
4 years ago |
|
Stefan Pranger
|
73e4945818
|
add STORM_DEVELOPER ALL_WARNINGS GCC case
non exhaustive in this commit, i.e. additional flags might be applicable
|
4 years ago |
|
Stefan Pranger
|
f106b83328
|
WIP added grammar rules for gameFormula
Does not compile at this stage! This commit will be squashed asap.
|
4 years ago |
|
Stefan Pranger
|
715784a070
|
added casting getter for gameFormula
|
4 years ago |
|
Stefan Pranger
|
8dc46968cb
|
added rPATL to FragmentSpecifitcations
|
4 years ago |
|
Stefan Pranger
|
c52fcba6a2
|
added multiple Visitor methods for gameFormulas
|
4 years ago |
|
Stefan Pranger
|
6dd9e09ede
|
added GameFormula class
|
4 years ago |
|
Stefan Pranger
|
cbbafaddfd
|
added Coalition class
will be used in rPATL formulas
|
4 years ago |
|
Stefan Pranger
|
2225ebcbe8
|
fix reorder warning
|
4 years ago |
|
Stefan Pranger
|
eba20bb005
|
switch cases in engine now feature SMG case
|
4 years ago |
|
Stefan Pranger
|
6a71c19d8a
|
added sparse smg model
|
4 years ago |
|
Stefan Pranger
|
bb05b9c03c
|
aggregate player indices into model
|
4 years ago |
|
Stefan Pranger
|
cea09f932b
|
generator now assigns player indices to states
|
4 years ago |
|
Stefan Pranger
|
163dfa8654
|
ModelComponents now feature a player mapping
|
4 years ago |
|
Stefan Pranger
|
6b715792aa
|
added player related helpers
|
4 years ago |
|
Stefan Pranger
|
160a2c32a2
|
added SMGs to existing ModelTypes
|
4 years ago |
|
Stefan Pranger
|
dce9496300
|
Model validity check now handles SMGs
|
4 years ago |
|
Stefan Pranger
|
9bf2a572a7
|
check if state is controlled by multiple players
We do this by storing a list of modules/commands which have already been claimed by one player
|
4 years ago |
|
Stefan Pranger
|
e9a6077acb
|
adapted player ostream output
|
4 years ago |
|
Stefan Pranger
|
1cf2e544ac
|
add assertion for module indices in second
|
4 years ago |
|
Stefan Pranger
|
de301323d6
|
check module and action names when parsing players
Note: This does currently not work as intended as the moduleToIndexMap
gets clear when moving to the second run!
|
4 years ago |
|
Stefan Pranger
|
43353d5243
|
store name index map for player member
|
4 years ago |
|
Stefan Pranger
|
271ed284a6
|
fix player ostream output
|
4 years ago |
|
Stefan Pranger
|
11f7464372
|
players now get stored in PRISM programs
|
4 years ago |
