 Stefan Pranger
|
81db530f70
|
do not clear moduleToIndexMap for second run
|
5 years ago |
|
Stefan Pranger
|
52e30059e3
|
fix reorder warning
|
5 years ago |
Tim Quatmann
|
e529045a8f
|
Merge commit '6a71c19d8a5808b3a0c5be21f0966e8ada7f4252' into smg-merge
|
5 years ago |
Sebastian Junges
|
4a7ea35959
|
first version for action mask callbacks in explicit generator
|
5 years ago |
|
Sebastian Junges
|
7a38f54d01
|
extend the next state generator to support prism program simulation
|
5 years ago |
|
Sebastian Junges
|
e5ed114715
|
a first simulator of prism files
|
5 years ago |
|
Sebastian Junges
|
aa6a3d2142
|
sampling from a distribution and from a choice
|
5 years ago |
|
Sebastian Junges
|
00a85cb184
|
accessors for model
|
5 years ago |
|
Stefan Pranger
|
b3f5cd1c89
|
fixed call of inherited function and
short curcuiting problem. Maybe && is overloaded somewhere?
|
5 years ago |
|
Stefan Pranger
|
0e79f71435
|
change optimization direction if overridden
|
5 years ago |
|
Stefan Pranger
|
50fdc36387
|
check convergence with weighted values
This is used for approximations for LRA MC for SMGs.
|
5 years ago |
|
Stefan Pranger
|
505c830d42
|
set optdir overrides from multiplier env
|
5 years ago |
|
Stefan Pranger
|
c7d7be8b83
|
nondetTs may also be gameNondetTs in LraViHelper
|
5 years ago |
|
Stefan Pranger
|
de385b0527
|
added method for lra game transition type
also added the according template class constructions.
|
5 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.
|
5 years ago |
|
Stefan Pranger
|
ea90c1ac7d
|
added and finalized methods for rpatlMC
|
5 years ago |
|
Stefan Pranger
|
f72f83f23e
|
computeLongRunAverageValues is now virtual
in SparseInfiniteHorizonHelper, since
SparseNondeterministicGameInfiniteHorizonHelper needs to overwrite it.
|
5 years ago |
|
Stefan Pranger
|
b61d947057
|
parse coalition operator and set row group optdirs
|
5 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.
|
5 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!)
|
5 years ago |
Matthias Volk
|
e610edc197
|
Run github actions daily
|
5 years ago |
Daniel Basgöze
|
741d04c797
|
Implement manually triggered github actions CI
|
5 years ago |
|
Stefan Pranger
|
af38bc3b4d
|
added transition type for games to LraViHelper
|
5 years ago |
|
Tim Quatmann
|
02695da9b7
|
Fixed several issues regarding powers with negative exponents.
|
5 years ago |
|
Tim Quatmann
|
a3ada8a0c3
|
cli: added a space that was missing in output of steady-state result
|
5 years ago |
|
Stefan Pranger
|
0a689d232e
|
init helper for games
|
5 years ago |
|
Stefan Pranger
|
19839036af
|
AbstractMC passes game formula to the rpatl MC
|
5 years ago |
|
Stefan Pranger
|
0a65e4aa7b
|
verification now handles SMGs
|
5 years ago |
|
Stefan Pranger
|
21af5c5d6a
|
handle model description ostream case for SMGs
|
5 years ago |
|
Stefan Pranger
|
b599ff5c7e
|
added sparse MC templates for SMGs
|
5 years ago |
|
Stefan Pranger
|
d1a0299bd0
|
buildMatrices handles playerIndices via reference
|
5 years ago |
|
Stefan Pranger
|
e88a83d9aa
|
engine now checks smg models
|
5 years ago |
|
Stefan Pranger
|
a299504361
|
added smg rpatl model checker
|
5 years ago |
|
Stefan Pranger
|
d939ebe375
|
smg model now stores the player action indices
|
5 years ago |
|
Stefan Pranger
|
353b98ec88
|
rpatl extends prctl
|
5 years ago |
|
Stefan Pranger
|
1470d65586
|
gameForumlas now gather referenced variables
|
5 years ago |
|
Tim Quatmann
|
4dcd1cfb64
|
Fixed simplification of expressions that use the power operator with negative exponents.
|
5 years ago |
|
Tim Quatmann
|
09cb0e5a5d
|
LraCtmcTest: Renamed a testcase as its name was misleading before.
|
5 years ago |
|
Tim Quatmann
|
5245d77bfc
|
SteadyState: Issue a warning in sound mode because it is not supported.
|
5 years ago |
|
Tim Quatmann
|
818f8cb8ee
|
steadystate: Added a testcase.
|
5 years ago |
|
Tim Quatmann
|
b73e2e5d1c
|
Fixing steady state distribution computation.
|
5 years ago |
|
Tim Quatmann
|
77d2e9c98f
|
Fixed output of steady-state distr computation.
|
5 years ago |
|
Tim Quatmann
|
211a72b6d7
|
fixing compilation of storm-pars
|
5 years ago |
|
Tim Quatmann
|
19e6473806
|
making the cudd warning sound a bit less dangerous
|
5 years ago |
|
Tim Quatmann
|
2e593dc014
|
Added computation of steady state probabilities for DTMC/CTMC in the sparse engine.
|
5 years ago |
|
Tim Quatmann
|
28ab011eb8
|
Added an export of check results to json.
|
5 years ago |
|
Tim Quatmann
|
84e6984659
|
StateValuations::toJson now has a template parameter to change the exported type of rationals.
|
5 years ago |
|
Tim Quatmann
|
75b6ac27e8
|
JaniParser: Making result field optional (fixes #83)
|
5 years ago |
|
Tim Quatmann
|
3184ba1611
|
Jani: Correctly parse the input-enable field. Throw an error in the sparse model builder, as these are not supported right now.
|
5 years ago |
|
Tim Quatmann
|
41ae9d5624
|
Fixed silently truncating bits when parsing integer literal expressions (see https://github.com/moves-rwth/stormpy/issues/20)
|
5 years ago |
