b3831d0093 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' into qcomp2020  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5d8419336f 
								
							
								 
							
						 
						
							
							
								
								InternalAdds: Added a comment related to GitHub issue  #64  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								36c410875c 
								
							
								 
							
						 
						
							
							
								
								Revert "InternalAdds: Making the different splitIntoGroups implementations more consistent to each other (in the sense that the Dd is traversed in the same order)."  
							
							
 
							
							
							This reverts commit cefe43f2bf#64  
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1f98f6c557 
								
							
								 
							
						 
						
							
							
								
								Reverted 'optimization' for Prob1Max (since that didn't work out).  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9d0d8022f9 
								
							
								 
							
						 
						
							
							
								
								Revert "Slight optimization in performProb1A"  
							
							
 
							
							
							This reverts commit 2df4679fbc 
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d288701e9d 
								
							
								 
							
						 
						
							
							
								
								Graph: Changed methods for prob1 methods in performProb1Max / performProb1Min to more efficient variants that can be used as we already know the prob0 states.  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								2df4679fbc 
								
							
								 
							
						 
						
							
							
								
								Slight optimization in performProb1A  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								fe5cd4db86 
								
							
								 
							
						 
						
							
							
								
								Fixed missing ;  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								99db5693ca 
								
							
								 
							
						 
						
							
							
								
								OVI: Implement upper bound only iterations  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a5d3d0e696 
								
							
								 
							
						 
						
							
							
								
								slight optimizations in the JaniNextStateGenerator  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f01d8943ad 
								
							
								 
							
						 
						
							
							
								
								Indicate if result is not fully correct due to abort  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3bb3ff9bc7 
								
							
								 
							
						 
						
							
							
								
								Support abortion in Unif+  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								45aa451be5 
								
							
								 
							
						 
						
							
							
								
								Signal handler supporting termination after waiting period  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								248c0ecd35 
								
							
								 
							
						 
						
							
							
								
								Improved performance of SCC Decomposition by avoiding memory (re-)allocations  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f56cdb1b93 
								
							
								 
							
						 
						
							
							
								
								OVI: Add upper bound only iterations option  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1c65a936c3 
								
							
								 
							
						 
						
							
							
								
								OVI: Use correct environment variable  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c016d0716e 
								
							
								 
							
						 
						
							
							
								
								OVI: Fixed edge case, if x = 0 and ub = 0  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3db9112a27 
								
							
								 
							
						 
						
							
							
								
								OVI: Introduced OVI as a minmax solver for topological solving  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								06787ab9c2 
								
							
								 
							
						 
						
							
							
								
								Added calls to setUrgentOptions for binaries  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6af34ffbe1 
								
							
								 
							
						 
						
							
							
								
								Removed old file  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								739d6a4420 
								
							
								 
							
						 
						
							
							
								
								OVI: Implement the guessing scaler factor option  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6ecee7e371 
								
							
								 
							
						 
						
							
							
								
								OVI: Add upper bound guessing scaler factor option  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								8b97895e24 
								
							
								 
							
						 
						
							
							
								
								OVI: More debug output & cross case assert  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								50a51a70c0 
								
							
								 
							
						 
						
							
							
								
								OVI: Debug output for inner interval iteration  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b1dc6fec06 
								
							
								 
							
						 
						
							
							
								
								Accelerated zeno check for MAs. Also only apply zeno check if --additional-checks is set.  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								bf99724f3b 
								
							
								 
							
						 
						
							
							
								
								Added missing include.  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								95b2095151 
								
							
								 
							
						 
						
							
							
								
								Implemented simplification of system composition (this enables compatibility for more benchmarks in the dd engine).  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								38439fc867 
								
							
								 
							
						 
						
							
							
								
								jani/Automaton: Implemented possibility to clone an automaton.  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4e7f8af851 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' into qcomp2020  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								141316943c 
								
							
								 
							
						 
						
							
							
								
								DdJaniModelBuilder: Also apply max. progress if the system consists of just a single automaton.  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5d530bb532 
								
							
								 
							
						 
						
							
							
								
								Improved compatibility of the dd-to-sparse engine (can now handle reward models with state action rewards)  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								eaacc6c0ac 
								
							
								 
							
						 
						
							
							
								
								Included the hybrid engine in the MA test.  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								cefe43f2bf 
								
							
								 
							
						 
						
							
							
								
								InternalAdds: Making the different splitIntoGroups implementations more consistent to each other (in the sense that the Dd is traversed in the same order).  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								7bf1abe136 
								
							
								 
							
						 
						
							
							
								
								Implemented LRA properties for the hybrid engine of MAs.  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e6597b35a6 
								
							
								 
							
						 
						
							
							
								
								OVI: Added a few settings to tweak ovi  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								50ff86e709 
								
							
								 
							
						 
						
							
							
								
								Polished/ improved ovi.  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f73be674a9 
								
							
								 
							
						 
						
							
							
								
								Update solver status if iterations exceeded  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								73b68836c5 
								
							
								 
							
						 
						
							
							
								
								Hybrid MA engine: (bounded) reachability probabilities  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								72eb58f73d 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'portfolio' into ma-hybrid  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a36e75db67 
								
							
								 
							
						 
						
							
							
								
								Fixed error introduced during merge  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								04c2938057 
								
							
								 
							
						 
						
							
							
								
								Introduced hybrid engine for Markov automata (only reach. rewards for now)  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								db697e7bfc 
								
							
								 
							
						 
						
							
							
								
								Split upper bound guessing for relative and absolute  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								33e21db8ea 
								
							
								 
							
						 
						
							
							
								
								Provide precision in bound guessing operation  
							
							
 
							
							
							OVI tested on consensus with all parameter options. 
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								cd15c01f2f 
								
							
								 
							
						 
						
							
							
								
								Relative and absolute error criterion  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								606087ce85 
								
							
								 
							
						 
						
							
							
								
								Absolute ub guessing and in-place center calculation  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b4e743c4a6 
								
							
								 
							
						 
						
							
							
								
								Also update lb in the verification phase  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								02a346b5b7 
								
							
								 
							
						 
						
							
							
								
								Fix: Set lb to ub if difference vector has no positive entry  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								444f737baa 
								
							
								 
							
						 
						
							
							
								
								Fix: Returning scaled vector  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a89c34f9de 
								
							
								 
							
						 
						
							
							
								
								Actually enable OVI in CLI  
							
							
								
 
							
							
						 
						6 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								94ed2556a8 
								
							
								 
							
						 
						
							
							
								
								Center calculation, variables moved for efficiency, removed booleans  
							
							
								
 
							
							
						 
						6 years ago