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
Matthias Volk
e610edc197
Run github actions daily
4 years ago
Daniel Basgöze
741d04c797
Implement manually triggered github actions CI
4 years ago
Tim Quatmann
02695da9b7
Fixed several issues regarding powers with negative exponents.
4 years ago
Tim Quatmann
a3ada8a0c3
cli: added a space that was missing in output of steady-state result
4 years ago
Tim Quatmann
4dcd1cfb64
Fixed simplification of expressions that use the power operator with negative exponents.
4 years ago
Tim Quatmann
09cb0e5a5d
LraCtmcTest: Renamed a testcase as its name was misleading before.
4 years ago
Tim Quatmann
5245d77bfc
SteadyState: Issue a warning in sound mode because it is not supported.
4 years ago
Tim Quatmann
818f8cb8ee
steadystate: Added a testcase.
4 years ago
Tim Quatmann
b73e2e5d1c
Fixing steady state distribution computation.
4 years ago
Tim Quatmann
77d2e9c98f
Fixed output of steady-state distr computation.
4 years ago
Tim Quatmann
211a72b6d7
fixing compilation of storm-pars
4 years ago
Tim Quatmann
19e6473806
making the cudd warning sound a bit less dangerous
4 years ago
Tim Quatmann
2e593dc014
Added computation of steady state probabilities for DTMC/CTMC in the sparse engine.
4 years ago
Tim Quatmann
28ab011eb8
Added an export of check results to json.
4 years ago
Tim Quatmann
84e6984659
StateValuations::toJson now has a template parameter to change the exported type of rationals.
4 years ago
Tim Quatmann
75b6ac27e8
JaniParser: Making result field optional ( fixes #83 )
4 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.
4 years ago
Tim Quatmann
41ae9d5624
Fixed silently truncating bits when parsing integer literal expressions (see https://github.com/moves-rwth/stormpy/issues/20 )
4 years ago
Tim Quatmann
51f86db9eb
Storm version 1.6.3
4 years ago
Tim Quatmann
7002946845
Updated changelog.
4 years ago
Tim Quatmann
251527bccf
storm-pars: Make a more explicit warning if a non-parametric equation solver type is selected.
4 years ago
Tim Quatmann
1243feba8c
Substitute constants in JANI Properties ( fixes #95 )
4 years ago
Tim Quatmann
065b366198
Removed superfluous '.' in output of Markov automata model data.
4 years ago
Tim Quatmann
6d6e142236
Fixed an issue with JANI models concerning properties using transient variable expressions.
4 years ago
Tim Quatmann
ee5fff680a
Indefinite Horizon helpers: Do not compute values of MaybeStates if they are not relevant for the property. ( Fixes #87 )
4 years ago
Tim Quatmann
20d424e289
JaniTraverser: Only traverse lower/upper bound expressions of BoundedIntegerVariables, if these bounds exists.
4 years ago
Tim Quatmann
ce0283d80d
Cmake: checked whether the stack-check issue still persists with current AppleClang v12.0.0
4 years ago
Tim Quatmann
8619a4d833
CMake: Implemented a workaround for building CUDD on MacOS Big Sur.
4 years ago
Tim Quatmann
1982dc0dba
SparsePcaaParetoQuery: Added a (hopefully explaining) comment
4 years ago