Tree: e1b00dae7a

main

tempestpy_adaptions

Branches Tags

${ item.name }

Create tag ${ searchTerm }

Create branch ${ searchTerm }

from 'e1b00dae7a'

${ noResults }

Commit Graph

180 Commits (e1b00dae7aaa18756055f35a1b20438491d9861f)

Author	SHA1	Message	Date
Stefan Pranger	679279a339	By changing the computation we now allow lowerBounds in bounded-globally formulas Conflicts: src/storm-parsers/parser/FormulaParserGrammar.cpp	4 years ago
Tim Quatmann	7e7d6defa0	Merge pull request #137 from tquatmann/ltl LTL Model Checking Also includes a reset of src/storm-parsers/parser/FormulaParserGrammar.cpp src/storm-parsers/parser/FormulaParserGrammar.h since there have been to many changes to fix them individually. Will follow up with a commit to introduce shield and smg formula parsing Conflicts: src/storm-parsers/parser/FormulaParserGrammar.cpp src/storm-parsers/parser/FormulaParserGrammar.h src/storm/logic/CloneVisitor.cpp src/storm/logic/Formula.h src/storm/logic/FragmentChecker.cpp src/storm/logic/FragmentSpecification.cpp src/storm/logic/FragmentSpecification.h src/storm/logic/LiftableTransitionRewardsVisitor.cpp src/storm/logic/ToPrefixStringVisitor.cpp src/storm/logic/ToPrefixStringVisitor.h src/storm/modelchecker/AbstractModelChecker.cpp src/storm/modelchecker/AbstractModelChecker.h src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp src/storm/storage/MaximalEndComponent.cpp src/storm/storage/Scheduler.cpp src/storm/storage/Scheduler.h src/storm/storage/jani/JSONExporter.cpp src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp	4 years ago
Stefan Pranger	7a851901e2	updates after cherry pick	4 years ago
Tim Quatmann	4cdd70949c	FormulaParser: HOA formulas shall only consider state-subformulas	4 years ago
Tim Quatmann	b71cb813df	FormulaParser: Fixed parsing of multi-bounded path operator and quantile operator	5 years ago
Tim Quatmann	4cf2fd7d61	Heavily refactored FormulaParser as it had become quite messy. LTL-Operator precedence should now correctly mimic the behavior of PRISM.	5 years ago
Joachim Klein	5482a32b8a	(LTL) Refactor unary/boolean state formulas to allow path formulas as well Previously, the formula parser only supported AND, OR and NOT over state formulas. For LTL, we need those over path formulas. We tweak the grammar, the AST types and visitors, to also handle UnaryBooleanPathFormula and BinaryBooleanPathformula. During parsing, we determine on-demand whether to generate the path or state formula variant by looking at the subformulas - if they are state formulas, the boolean operator will be a state formula as well. Conflicts: src/storm-parsers/parser/FormulaParserGrammar.cpp src/storm-parsers/parser/FormulaParserGrammar.h src/storm/logic/CloneVisitor.cpp src/storm/logic/Formula.cpp src/storm/logic/Formula.h src/storm/logic/FragmentChecker.cpp src/storm/logic/FragmentSpecification.cpp src/storm/logic/FragmentSpecification.h src/storm/logic/LiftableTransitionRewardsVisitor.cpp src/storm/storage/jani/JSONExporter.cpp	5 years ago
Joachim Klein	ad774e5138	WIP (HOA-path) FormulaParser: parse HOAPathFormula Note: Syntax of HOA path formulas will change! Conflicts: src/storm-parsers/parser/FormulaParserGrammar.cpp src/storm-parsers/parser/FormulaParserGrammar.h	5 years ago
Joachim Klein	ba907a1d75	WIP (HOA-path) FormulaParser: parse HOAPathFormula Note: Syntax of HOA path formulas will change! Conflicts: src/storm-parsers/parser/FormulaParserGrammar.cpp src/storm-parsers/parser/FormulaParserGrammar.h	5 years ago
Stefan Pranger	9b6afac4d7	renamed factors for shielding to probabilities	4 years ago
Stefan Pranger	f9d2df0b0a	move ConstantDataType and added ostream	4 years ago
Stefan Pranger	d749b3c46a	allow optional 'Shield' string when parsing ShieldExpressions	4 years ago
Tim Quatmann	aa5bb9cb7d	PrismParser: Parsing unbounded integer variables	5 years ago
Stefan Pranger	0479b58472	added names and optimal shield to parsing	5 years ago
Stefan Pranger	d9db7d57b3	parsing ShieldExpression into shared_ptr	5 years ago
Stefan Pranger	d4d3c0d9ea	Jani Props may now hold info about shielding query	5 years ago
Stefan Pranger	fa47742a14	added checks for multiplicative factor parsing	5 years ago
Stefan Pranger	f6b341168d	added formula parser grammar for shields	5 years ago
Lukas Posch	5e040553a6	changed error message	5 years ago
Lukas Posch	0ea549864f	fixed assert for using lowerBounds	5 years ago
Lukas Posch	02bc7f3f69	added assert for using lowerBounds	5 years ago
Lukas Posch	66f893edcb	changed globally formula grammar and added the case for bounded globally formulas for createGloballyFormula	5 years ago
Lukas Posch	023e067c59	added bounded globally formulas to other classes	5 years ago
Sebastian Junges	c4187b03eb	fixed error messages	5 years ago
Matthias Volk	9fea07542a	Fixed warning	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
Stefan Pranger	8b74f49806	fixup after merging PRs	5 years ago
Stefan Pranger	fae507c902	removed residual loc from rebase	5 years ago
Stefan Pranger	40f5fc04a9	rpatl smg formulas now accept operatorFormulas	5 years ago
Stefan Pranger	f9368be970	refactor Coalition to use boost variant	5 years ago
Stefan Pranger	de38996b4e	add assertion for module indices in second	5 years ago
Stefan Pranger	07d7ca9189	WIP added grammar rules for gameFormula Does not compile at this stage! This commit will be squashed asap.	5 years ago
Tim Quatmann	c2fc1218b7	JaniParser: Make warning disappear when assigning an int expression to a real-valued function.	5 years ago
Tim Quatmann	9b05861324	JaniParser: Fixed a syntax check.	5 years ago
Stefan Pranger	e63faa485f	changed format of player parsing exceptions	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
Stefan Pranger	6c97e9dc29	rpatl smg formulas now accept operatorFormulas	5 years ago
Stefan Pranger	8d47ad2bd7	refactor Coalition to use boost variant	5 years ago
Stefan Pranger	487eb13a24	WIP added grammar rules for gameFormula Does not compile at this stage! This commit will be squashed asap.	5 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)	5 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	5 years ago
Stefan Pranger	81db530f70	do not clear moduleToIndexMap for second run	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
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
Stefan Pranger	6cea196953	rpatl smg formulas now accept operatorFormulas	5 years ago
Tim Quatmann	1243feba8c	Substitute constants in JANI Properties (fixes #95)	5 years ago