Tree: 48d37ccc50

tempestpy_adaptions

Branches Tags

${ item.name }

Create tag ${ searchTerm }

Create branch ${ searchTerm }

from '48d37ccc50'

${ noResults }

Commit Graph

9477 Commits (48d37ccc502c0fbd3739756f3accd445aa57d32a)

 

All Branches   

Search

Author	SHA1	Message	Date
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	4 years ago
Joachim Klein	256f9839da	SparseDtmcPrctlModelChecker: computeDAProductProbabilities()	4 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	4 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	4 years ago
Joachim Klein	aed8e53a29	(HOA-path) AbstractModelChecker: default handling for HOAPathFormulas (= reject) Conflicts: src/storm/modelchecker/AbstractModelChecker.h	4 years ago
Joachim Klein	21b9d73816	WIP (HOA-path) logic: HOAPathFormula Note: syntax of the HOA path formula will change! We have added checks for boundedGloballyFormulae hence the conflicts Conflicts: src/storm/logic/CloneVisitor.cpp src/storm/logic/Formula.cpp src/storm/logic/Formula.h src/storm/logic/FragmentSpecification.cpp src/storm/logic/FragmentSpecification.h src/storm/logic/LiftableTransitionRewardsVisitor.cpp src/storm/storage/jani/JSONExporter.cpp	4 years ago
Joachim Klein	85a408dd72	(DA-product) tests: DAProductBuilderTest	4 years ago
Stefan Pranger	044074a4b1	(DA) tests: HOAParsingTest	3 years ago
Joachim Klein	e5282708dd	(DA-product) transformer: Product, DAProduct + builders	4 years ago
Joachim Klein	3696e13736	(DA) ItemLabeling: addUniqueLabel, generateUniqueLabel For model-automaton product constructions, we would like to add automatically generated labels to the result, so we need a way to ensure that we can get those without clashing with existing labels.	4 years ago
Joachim Klein	de0dd71679	(DA) Automata classes: DeterministicAutomaton, APSet, HOAConsumer, AcceptanceCondition Adapted from ltl2dstar.	4 years ago
Joachim Klein	8d680749cd	(DA) Add cpphoafparser 0.99.2 Add cpphoafparser 0.99.2 as 3rdparty library (for HOA automata parsing).	4 years ago
Stefan Pranger	f4fb0188be	Merge pull request 'Adapt Property Ctors with ShieldingExpression Parameter' (#44) from storm_prs_and_updates into main Reviewed-on: https://git.pranger.xyz/TEMPEST/tempest-devel/pulls/44	3 years ago
Stefan Pranger	b53a255365	adapted property ctors with ShieldingExpression param	3 years ago
Stefan Pranger	d3e313dcb4	Merge pull request '[STORM PR] Summary' (#43) from storm_prs_and_updates into main Reviewed-on: https://git.pranger.xyz/TEMPEST/tempest-devel/pulls/43	3 years ago
Lukas Posch	9d4e654ec2	fix for quantitative computations in computeUntilProb	3 years ago
Stefan Pranger	d88feb18ea	Merge remote-tracking branch 'storm_gh/master' into storm_prs_and_updates Conflicts: .github/workflows/buildtest.yml .github/workflows/doxygen.yml src/storm/builder/ExplicitModelBuilder.h src/storm/generator/Choice.cpp src/storm/generator/Choice.h src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp	3 years ago
Tim Quatmann	4dfb2a959f	Updated Author list in Readme.md	3 years ago
Stefan Pranger	e8c24ec532	Merge pull request 'Shields for MDPs' (#24) from mdp_shields into main Reviewed-on: https://git.pranger.xyz/TEMPEST/tempest-devel/pulls/24	3 years ago
Stefan Pranger	6a5f626259	refactored helper code	3 years ago
Stefan Pranger	b686bfebb0	remove whitespaces and debug output	3 years ago
Stefan Pranger	e6eed7cbc4	moved computation out of if/else	3 years ago
Lukas Posch	1599034b5c	fixed shield handling	3 years ago
Lukas Posch	7cbe2886eb	fixed shield handling for MDP Next and BoundedGlobally	3 years ago
Lukas Posch	591e63e11e	fixed choiceValues for MDP shields - Until and Globally	3 years ago
Lukas Posch	78a3b2a6a7	Nullpointer check for dirOverride	3 years ago
Lukas Posch	444929a9a3	create MDP shields if it is a shielding task	3 years ago
Lukas Posch	76a34bc957	expanded compute method in SparseNondeterministicStepBoundedHorizonHelper.* with resultMaybestates and choiceValues	3 years ago
Lukas Posch	def9e65525	store the choiceValues in the iterations and the maybeStates then return it to the SparseMdpPrctlModelChecker.cpp	3 years ago
Lukas Posch	053f0a8d19	extended MDPModelCheckingHelperReturnType with maybeStates and choiceValues	3 years ago
Lukas Posch	222a18a760	added methods reduce and repeatedMultiplyAndReduceWithChoices to Multiplier.* to store the choiceValues between multiply and reduce Also fixed the call to goal isShieldingTask in SMG Helpers	3 years ago
Lukas Posch	731c060c4e	added method isShieldingTask() to SolveGoal.*	3 years ago
Lukas Posch	79447073d0	changed shield-handling.h to ShieldHandling.cpp and ShieldHandling.h renamed createOptimalShield() to createQuantitativShield()	3 years ago
Stefan Pranger	a63d8cda6b	Merge pull request 'Flip Bits when Passing CoalitionStates to ShieldHandling' (#29) from fix_formula_parser_debug into main Reviewed-on: https://git.pranger.xyz/TEMPEST/tempest-devel/pulls/29	3 years ago
Stefan Pranger	bb6cd2232f	flip bits when passing coalition to shieldhandling	4 years ago
Stefan Pranger	6f19aaea7f	Merge pull request 'Introduce Shields' (#16) from safety_shields into main Reviewed-on: https://git.pranger.xyz/TEMPEST/tempest-devel/pulls/16	3 years ago
Stefan Pranger	4746a81b51	removed output and check in checkGameFormula	3 years ago
Stefan Pranger	8ffcabc79d	fixed error messages in shield handling	3 years ago
Stefan Pranger	8304c897cd	refactored creation of coalitionStates	3 years ago
Sebastian Junges	6e8387235d	Merge pull request #120 from sjunges/master Long-living branch merge (POMDPs, Prism-Language Simulation, bug fixes)	3 years ago
Stefan Pranger	774299bdc2	removed commented code from Property	3 years ago
Stefan Pranger	b73b0b2a75	removed unused code and added method desc	3 years ago
Stefan Pranger	a8d6b5e874	removed unused code from MultiplierEnv	3 years ago
Stefan Pranger	6bd625e4c8	removed debug output also introduced changes to be made as soon as 4fd42356d0 is merged	3 years ago
Stefan Pranger	9b6afac4d7	renamed factors for shielding to probabilities	3 years ago
Stefan Pranger	1d5eba326d	removed comment from PostScheduler	3 years ago
Stefan Pranger	29fb202761	cleaned up GameVi and LraViHelper	3 years ago
Stefan Pranger	f77293de78	added comments for CheckTask methods	3 years ago
Stefan Pranger	dadcda9f0c	Merge pull request 'Fix Formula Parser Debug Methods' (#25) from formula_parser_debug into main Reviewed-on: https://git.pranger.xyz/TEMPEST/tempest-devel/pulls/25	3 years ago
Stefan Pranger	f9d2df0b0a	move ConstantDataType and added ostream	3 years ago