Tim Quatmann
d1b068eddf
specified supported rpatl fragment a bit more precisely
4 years ago
Stefan Pranger
01ed518ab3
AbstractMC passes game formula to the rpatl MC
4 years ago
Stefan Pranger
8dee62cbdd
added sparse MC templates for SMGs
4 years ago
Stefan Pranger
ace401f120
added smg rpatl model checker
4 years ago
Tim Quatmann
f28e59ab8d
Polished SMG model
4 years ago
Tim Quatmann
109a885c65
PlayerCoalition: Added a getter for players
4 years ago
Tim Quatmann
4affb76bb1
Renamed Coalition to more descriptive PlayerCoalition
4 years ago
Tim Quatmann
735874462c
Polished fragment specification and formula visitors for new GameFormulas
4 years ago
Tim Quatmann
4c5bc4e2a2
Polished GameFormula and Coalition code
4 years ago
Tim Quatmann
2cf73f9b10
ModelType: Fixed capitalization of SMG output
4 years ago
Stefan Pranger
4d4cd6e7f4
rpatl extends prctl
4 years ago
Stefan Pranger
8e55ec62ad
gameForumlas now gather referenced variables
4 years ago
Stefan Pranger
6c97e9dc29
rpatl smg formulas now accept operatorFormulas
4 years ago
Stefan Pranger
8d47ad2bd7
refactor Coalition to use boost variant
4 years ago
Stefan Pranger
2972f43def
removed print from CloneVisitor
4 years ago
Stefan Pranger
3f2aaf72b0
fixed typo in arg list of GameFormula
4 years ago
Stefan Pranger
2721f24b9b
added Coalition default ctor
4 years ago
Stefan Pranger
487eb13a24
WIP added grammar rules for gameFormula
Does not compile at this stage! This commit will be squashed asap.
4 years ago
Stefan Pranger
df52e5af88
added casting getter for gameFormula
4 years ago
Stefan Pranger
2f5a53196c
added rPATL to FragmentSpecifitcations
4 years ago
Stefan Pranger
7d87a90c1e
added multiple Visitor methods for gameFormulas
4 years ago
Stefan Pranger
09cb1d465c
added GameFormula class
4 years ago
Stefan Pranger
310c9d21d4
added Coalition class
will be used in rPATL formulas
4 years ago
Stefan Pranger
bc5eec34d2
switch cases in engine now feature SMG case
4 years ago
Tim Quatmann
875410a59e
Polished ExplicitModelBuilder:
* ChoiceInformationBuilder renamed to StateAndChoiceInformationBuilder, now also keeping track of state-based information (StateValuations, MarkovianStates, statePlayerIndications)
* ModelComponents now consider statePlayerIndications and PlayerNamesToIndices separately
4 years ago
Tim Quatmann
277f802850
* PlayerIndex is now declared in a separate file (as this can potentially be independent of PRISM input).
* Polished PrismNextStateGenerator, in particular more proper error handling
4 years ago
Matthias Volk
3ba9ae637c
Run doxygen deploy on push and do not keep history
4 years ago
Daniel Basgöze
d2c6420356
Add doxygen deploy workflow
currently manually triggered
4 years ago
Daniel Basgöze
df721f55d7
Cleanup comments
4 years ago
Tim Quatmann
97b2d751e0
* prism::Player's no longer keep track of module and action indices to reduce redundancies.
* PrismProgram::CheckValidity and PrismProgram::simplify now treat SMGs properly
* PrismProgram is now responsible for moduleIndex->playerIndex and actionIndex->playerIndex assignment
* More defined behavior for actions that don't have a player (work in progress)
4 years ago
Tim Quatmann
6fe76a009d
Polished parsing of Prism-SMGs, in particular
* Fixed issues related to module renaming that resulted from setting the module indices already in the first run
* Fixed a few uint_fast32_t vs uint_fast64_t issues, created alias PlayerIndex
4 years ago
Stefan Pranger
81db530f70
do not clear moduleToIndexMap for second run
4 years ago
Stefan Pranger
52e30059e3
fix reorder warning
4 years ago
Tim Quatmann
e529045a8f
Merge commit '6a71c19d8a5808b3a0c5be21f0966e8ada7f4252' into smg-merge
4 years ago
Sebastian Junges
4a7ea35959
first version for action mask callbacks in explicit generator
4 years ago
Sebastian Junges
7a38f54d01
extend the next state generator to support prism program simulation
4 years ago
Sebastian Junges
e5ed114715
a first simulator of prism files
4 years ago
Sebastian Junges
aa6a3d2142
sampling from a distribution and from a choice
4 years ago
Sebastian Junges
00a85cb184
accessors for model
4 years ago
Stefan Pranger
b3f5cd1c89
fixed call of inherited function and
short curcuiting problem. Maybe && is overloaded somewhere?
4 years ago
Stefan Pranger
0e79f71435
change optimization direction if overridden
4 years ago
Stefan Pranger
50fdc36387
check convergence with weighted values
This is used for approximations for LRA MC for SMGs.
4 years ago
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