Lukas Posch 
							
						 
						
							
							
							
								
							
								90568c54a2 
								
							
								 
							
						 
						
							
							
								
								added RewardOperatorTest to GameFormulaParserTest.cpp  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								442ffecd13 
								
							
								 
							
						 
						
							
							
								
								created NextOperatorTest in GameFormulaParserTest.cpp  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								bc6dabb088 
								
							
								 
							
						 
						
							
							
								
								fixed UntilOperatorTest in GameFormulaParserTest.cpp  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								45319ca2da 
								
							
								 
							
						 
						
							
							
								
								WIP GameFormulaParserTest.cpp  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								f1aa210b5a 
								
							
								 
							
						 
						
							
							
								
								shielding check for FragmentCheckerTest Prctl  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								d8592bffa2 
								
							
								 
							
						 
						
							
							
								
								shielding check for FragmentCheckerTest Rpatl  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								868f42b38b 
								
							
								 
							
						 
						
							
							
								
								Bounded LTL formula check for FragmentCheckerTest Rpatl  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								e1b00dae7a 
								
							
								 
							
						 
						
							
							
								
								small change in FragmentCheckerTest Rpatl  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								1b81c009c1 
								
							
								 
							
						 
						
							
							
								
								WIP added GameFormulaParserTest.cpp  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								04dd2b2e92 
								
							
								 
							
						 
						
							
							
								
								added a smg to PrismParserTest.cpp  
							
							 
							
							 
							
							
								
 
							
							
							Conflicts:
	src/test/storm/parser/PrismParserTest.cpp 
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								d14b04fe72 
								
							
								 
							
						 
						
							
							
								
								WIP DEBUG message for multiplier type  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								3a91b266d4 
								
							
								 
							
						 
						
							
							
								
								WIP expanded tests, now tests run for X, U, G, F  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								b49dd59101 
								
							
								 
							
						 
						
							
							
								
								WIP added testcases for globally probabilities for SmgRpatlModelCheckerTest "Walker"  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								d0f85313f3 
								
							
								 
							
						 
						
							
							
								
								added probabalisticFormula.rpatl in testfolder for rpatl for future purposes  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								fdb84fdee5 
								
							
								 
							
						 
						
							
							
								
								changed the info about statesOfCoalition to STORM_LOG_INFO  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								7565bc5d6a 
								
							
								 
							
						 
						
							
							
								
								created SmgRpatlModelCheckerTest.cpp as test suite for rpatl smg models  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								a7919a651c 
								
							
								 
							
						 
						
							
							
								
								added a smg example for checking test-modelchecker-rpatl-smg  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								3d73e71162 
								
							
								 
							
						 
						
							
							
								
								introduced test-modelchecker-rpatl-smg  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								8d11ed9f42 
								
							
								 
							
						 
						
							
							
								
								added first rpatl fragment checker tests  
							
							 
							
							 
							
							
								
 
							
							
							Conflicts:
	src/test/storm/logic/FragmentCheckerTest.cpp 
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								9a0be7e9ca 
								
							
								 
							
						 
						
							
							
								
								added first rpatl fragment checker tests  
							
							 
							
							 
							
							
								
 
							
							
							Conflicts:
	src/test/storm/logic/FragmentCheckerTest.cpp 
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								fc18ea12d3 
								
							
								 
							
						 
						
							
							
								
								Merge pull request 'Cleanup SMG RPATL Model Checking' ( #34 ) from smg_cleanup into main  
							
							 
							
							 
							
							
								
 
							
							
							Reviewed-on: https://git.pranger.xyz/TEMPEST/tempest-devel/pulls/34  
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								1391b26e93 
								
							
								 
							
						 
						
							
							
								
								Removed unnecessary debug information  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								fb84fc6af0 
								
							
								 
							
						 
						
							
							
								
								Added a comment why this computeBoundedGlobally check happens.  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								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  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								86c3b3d9c6 
								
							
								 
							
						 
						
							
							
								
								changed computeBoundedGloballyProbabilities computation by using computeBoundedUntilProbabilities  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								4373c324f9 
								
							
								 
							
						 
						
							
							
								
								checks for bounds in SparseSmgRpatlModelChecker  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								9fea23981a 
								
							
								 
							
						 
						
							
							
								
								finished computeBoundedUntilProbability in SparseSmgRpatlHelper  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								03ec53321e 
								
							
								 
							
						 
						
							
							
								
								added updateStatesOfCoalition to GameViHelper  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								fefd6b0951 
								
							
								 
							
						 
						
							
							
								
								WIP helper functions in GameViHelper  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								c2d2c38c28 
								
							
								 
							
						 
						
							
							
								
								WIP computeBoundedUntilProbabilities in SparseSmgRpatlHelper  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								28252a3caf 
								
							
								 
							
						 
						
							
							
								
								added computeBoundedUntilProbabilities to SparseSmgRpatlModelChecker  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								44d83b9fe0 
								
							
								 
							
						 
						
							
							
								
								added checks for bounds in computeBoundedGloballyProbabilities  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								3f408d059c 
								
							
								 
							
						 
						
							
							
								
								allow boundedUntilFormulas in rpatl  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								75bacaa6b2 
								
							
								 
							
						 
						
							
							
								
								deleted BoundedGloballyGameViHelper  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								e5dd9ab90f 
								
							
								 
							
						 
						
							
							
								
								small cleanup SparseSmgRpatlModelChecker  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								f4615614c1 
								
							
								 
							
						 
						
							
							
								
								use GameViHelper instead of BoundedGloballyGameViHelper  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								d222337715 
								
							
								 
							
						 
						
							
							
								
								added functionality of BoundedGloballyGameViHelper to GameViHelper  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								6289788a68 
								
							
								 
							
						 
						
							
							
								
								small changes to fit to the GameViHelper.*  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								65a5308809 
								
							
								 
							
						 
						
							
							
								
								small change in computation in computeNextProbabilities  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								b6ffa9a649 
								
							
								 
							
						 
						
							
							
								
								small change in the comments of computeGloballyProbabilities  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								7bdb5e11a8 
								
							
								 
							
						 
						
							
							
								
								fixed case for empty relevantStates in computeBoundedGlobally Probabilities  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Lukas Posch 
							
						 
						
							
							
							
								
							
								8301c3dc88 
								
							
								 
							
						 
						
							
							
								
								fixed case for empty relevantStates in computeUntilProbabilities  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								6c6f501900 
								
							
								 
							
						 
						
							
							
								
								Merge pull request '[STORM PR] Fixes after LTL merge' ( #47 ) from merge_pr_137 into main  
							
							 
							
							 
							
							
								
 
							
							
							Reviewed-on: https://git.pranger.xyz/TEMPEST/tempest-devel/pulls/47  
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								90dba4cd5d 
								
							
								 
							
						 
						
							
							
								
								adapted mdpprctlhelper call in MA model checker  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								c19639d156 
								
							
								 
							
						 
						
							
							
								
								added missing method to visitor  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								d53fafa078 
								
							
								 
							
						 
						
							
							
								
								fixed some changes which have been overwritten  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								85c5125610 
								
							
								 
							
						 
						
							
							
								
								removed duplicate code after big merge  
							
							 
							
							
								
 
							
							
						 
						4 years ago  
					 
				
					
						
							
							
								
									
								
								Stefan Pranger 
							
						 
						
							
							
							
								
							
								814f7b036d 
								
							
								 
							
						 
						
							
							
								
								Merge pull request '[STORM PR] LTL Model Checking#137' ( #45 ) from merge_pr_137 into main  
							
							 
							
							 
							
							
								
 
							
							
							Reviewed-on: https://git.pranger.xyz/TEMPEST/tempest-devel/pulls/45  
							
						 
						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  
					 
				
					
						
							
							
								 
								Tim Quatmann
							
						 
						
							
							
							
								
							
								3d96b0728d 
								
							
								 
							
						 
						
							
							
								
								CI: Use spot in all existing configurations. Add a new configuration without Spot.  
							
							 
							
							
								
 
							
							
						 
						4 years ago