Sebastian Junges
a5842e4a61
nasty bug where some sync action indices where not reflected in one of the data structures
5 years ago
Sebastian Junges
7daa5e2ab7
fixed error message
5 years ago
Matthias Volk
7111674ec8
Support for simulation of PDEP
5 years ago
Sebastian Junges
42ec9ec60d
state lookup does not crash when state does not exist
5 years ago
Sebastian Junges
c1ec3032fa
reset to state
5 years ago
Tim Quatmann
6d24ea9606
Silenced many 'loop variable is always a copy' warnings
5 years ago
Tim Quatmann
481d23b904
Replaced storm::expressions::Expression::operator^ by storm::expressions::pow. An optional flag indicates if we should allow power expressions of integer type (PRISM semantics) or whether it is always a real (JANI semantics).
5 years ago
Tim Quatmann
46462d6556
Z3Adapter: Fixing translation of XOR operators - expression's operator^ is supposed to be power, not xor.
5 years ago
Tim Quatmann
d863fe4156
Jani Export: Power expressions of integer type need to be type casted.
5 years ago
Jip Spel
5a37a40cea
Monotonicity for computing extremal value and parameter space partitioning
5 years ago
Matthias Volk
d6d36ee557
Support for sampling from exponential distribution
5 years ago
Tim Quatmann
8b68fbf948
JaniBuilder: Fixed checks for transient variable assignments
5 years ago
Matthias Volk
b0f6a192d4
Added missing include
5 years ago
Tim Quatmann
44be19f274
Added missing treatment of SMGs in API method.
5 years ago
Tim Quatmann
d82f5353ad
Fixed includes of RPATL model checker.
5 years ago
Tim Quatmann
579ab274e6
Fixed computing coalition states in SMG.
5 years ago
Tim Quatmann
a0a1bb629c
Fixing call of checkGameFormula
5 years ago
Tim Quatmann
792956deb9
Fixing output of player construct.
5 years ago
Tim Quatmann
e0977ebb81
Fixed buildActionIndexToPlayerIndexMap
5 years ago
Tim Quatmann
efce929c5f
Potentially allow verification of SMGs over RationalNumbers
5 years ago
Stefan Pranger
6701c61178
verification now handles SMGs
5 years ago
Tim Quatmann
6473645802
engine: changed order in enumeration for consistency
5 years ago
Stefan Pranger
2cfe0fa5d8
handle model description ostream case for SMGs
5 years ago
Stefan Pranger
c8fd980544
engine now checks smg models
5 years ago
Tim Quatmann
6c0cbe622f
Polished SparseSmgRpatlModelChecker
5 years ago
Tim Quatmann
fe4ef46f6b
CheckTask now stores player coalition.
5 years ago
Tim Quatmann
d1b068eddf
specified supported rpatl fragment a bit more precisely
5 years ago
Stefan Pranger
01ed518ab3
AbstractMC passes game formula to the rpatl MC
5 years ago
Stefan Pranger
8dee62cbdd
added sparse MC templates for SMGs
5 years ago
Stefan Pranger
ace401f120
added smg rpatl model checker
5 years ago
Tim Quatmann
f28e59ab8d
Polished SMG model
5 years ago
Tim Quatmann
109a885c65
PlayerCoalition: Added a getter for players
5 years ago
Tim Quatmann
4affb76bb1
Renamed Coalition to more descriptive PlayerCoalition
5 years ago
Tim Quatmann
735874462c
Polished fragment specification and formula visitors for new GameFormulas
5 years ago
Tim Quatmann
4c5bc4e2a2
Polished GameFormula and Coalition code
5 years ago
Tim Quatmann
2cf73f9b10
ModelType: Fixed capitalization of SMG output
5 years ago
Stefan Pranger
4d4cd6e7f4
rpatl extends prctl
5 years ago
Stefan Pranger
8e55ec62ad
gameForumlas now gather referenced variables
5 years ago
Stefan Pranger
8d47ad2bd7
refactor Coalition to use boost variant
5 years ago
Stefan Pranger
2972f43def
removed print from CloneVisitor
5 years ago
Stefan Pranger
3f2aaf72b0
fixed typo in arg list of GameFormula
5 years ago
Stefan Pranger
2721f24b9b
added Coalition default ctor
5 years ago
Stefan Pranger
df52e5af88
added casting getter for gameFormula
5 years ago
Stefan Pranger
2f5a53196c
added rPATL to FragmentSpecifitcations
5 years ago
Stefan Pranger
7d87a90c1e
added multiple Visitor methods for gameFormulas
5 years ago
Stefan Pranger
09cb1d465c
added GameFormula class
5 years ago
Stefan Pranger
310c9d21d4
added Coalition class
will be used in rPATL formulas
5 years ago
Stefan Pranger
bc5eec34d2
switch cases in engine now feature SMG case
5 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
5 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
5 years ago