9fea07542a
Fixed warning
4 years ago
6d24ea9606
Silenced many 'loop variable is always a copy' warnings
4 years ago
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).
4 years ago
c2fc1218b7
JaniParser: Make warning disappear when assigning an int expression to a real-valued function.
4 years ago
9b05861324
JaniParser: Fixed a syntax check.
4 years ago
4affb76bb1
Renamed Coalition to more descriptive PlayerCoalition
4 years ago
735874462c
Polished fragment specification and formula visitors for new GameFormulas
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
487eb13a24
WIP added grammar rules for gameFormula
Does not compile at this stage! This commit will be squashed asap.
4 years ago
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
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
75b6ac27e8
JaniParser: Making result field optional ( fixes #83 )
4 years ago
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
41ae9d5624
Fixed silently truncating bits when parsing integer literal expressions (see https://github.com/moves-rwth/stormpy/issues/20 )
4 years ago
1243feba8c
Substitute constants in JANI Properties ( fixes #95 )
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
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
11f7464372
players now get stored in PRISM programs
4 years ago
Stefan Pranger
48276e47a9
further work on player parsing
we do now correctly store command and modules names passed within a player
construct
4 years ago
Stefan Pranger
3f3b154ce0
first progress on player parsing
WIP. This does currently not compile, having troubles with the parsing
of command and module names into their resp. vectors.
4 years ago
Stefan Pranger
55f4efd40a
added SMG ModelType
4 years ago
Stefan Pranger
d35e9a6a40
removed plenty of empty line whitespaces
4 years ago
c12c0352f7
Support for parsing jani model from string
4 years ago
260c14a3f6
ExpressionParser: Allow sequences of unary operators, like '!!x=0' ( fixes #89 )
4 years ago
d6bfcb4818
refactoring: moving some code out of the util folder
5 years ago
0eec9e56da
better error message when a colon cannot be found in the drn file
5 years ago
65fab09931
comments in the model are now also allowed
5 years ago
a61ea32aea
Fixed some GCC warnings
5 years ago
1dccab9673
JaniParser: Added missing template instantiation and other fixes.
5 years ago
0433469b9e
Added missing template instantiation.
5 years ago
7b32aa968e
Fixed actually using the JaniParser with rational numbers.
5 years ago
328b9c6986
Gave the JaniParser a template argument, so that we can use it to parse with doubles or with RationalNumbers.
5 years ago
6f62e8d402
Support abort in model building
5 years ago
6c095e757a
Fixed problem with Windows linebreak \r\n, because this is still a problem in 2020
5 years ago
18bfe74d8f
api/model_descriptions: Fixed ambiguous method declaration.
5 years ago
d36cd93ae8
CLI: Split parsing and preprocessing of symbolic input into two steps.
Moved engine related methods and declaration to a separate file.
5 years ago
0a6f54f33e
a version of parsing choice labels from DRN
5 years ago
cb2e22e1d3
improved error message if observables includes an unknown error variable
5 years ago
290ede7404
extended the parser to handle observable expressions
5 years ago
b1bb7872fd
Parsing integers as long long ints (instead of ints) to fix github issue #60 .
5 years ago
bc85e6742e
Fixed parsing of RationalFunctions if no parameters are given
5 years ago
b24d224691
tests: Enabled logging output while running test-cases.
5 years ago
7c535cca84
Fixed upcasting of Exceptions in PrismParser.
5 years ago
4ee31063a4
Removed double whitespaces in outputs
5 years ago
78d99328b6
PrismParser: Making module renaming a LocatedInformation so we can properly store the line number of it. Also silenced a warning related to virtual destructors
5 years ago
3db50f570d
PrismProgram: Correctly set line numbers for renamed modules.
5 years ago
5f3065ec5a
PrismParser: Check for expression type. Support for formulas in arbitrary order.
5 years ago
Matthias Volk
Tim Quatmann
Stefan Pranger
Sebastian Junges
Sebastian Junges