00f88ed452 
								
							
								 
							
						 
						
							
							
								
								gauss-seidel-style value iteration  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9d95d2adcf 
								
							
								 
							
						 
						
							
							
								
								first version of multiply-and-reduce (only for native)  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e37d5869ef 
								
							
								 
							
						 
						
							
							
								
								extracted static version to separate cmake file  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								dd035f7f5e 
								
							
								 
							
						 
						
							
							
								
								allow for summand in matrix-vector multiplication  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3c844a487f 
								
							
								 
							
						 
						
							
							
								
								some more optimizations  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5fafe835cb 
								
							
								 
							
						 
						
							
							
								
								started on some optimizations for conditionals in MDPs  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								45e0796228 
								
							
								 
							
						 
						
							
							
								
								updated changelog  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								cffc3e606e 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' into solver_requirements  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b7e2aec82c 
								
							
								 
							
						 
						
							
							
								
								Fixed issue where variable names were reserved symbols of Exprtk  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								83fdffadc6 
								
							
								 
							
						 
						
							
							
								
								adapted tests; in particular enabled previously disabled rewards test  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9bda631795 
								
							
								 
							
						 
						
							
							
								
								symbolic MDP helper respecting solver requirements  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								7c24607427 
								
							
								 
							
						 
						
							
							
								
								started on symbolic solver requirements  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e81d979d56 
								
							
								 
							
						 
						
							
							
								
								hybrid MDP helper respecting solver requirements  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a3cbaedcc1 
								
							
								 
							
						 
						
							
							
								
								intermediate commit to switch workplace  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								12b10af672 
								
							
								 
							
						 
						
							
							
								
								started on hybrid MDP helper respecting solver requirements  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3c4de8ace3 
								
							
								 
							
						 
						
							
							
								
								moved requirements to new file  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4c5cdfeafc 
								
							
								 
							
						 
						
							
							
								
								Sparse MDP helper now also respects solver requirements for reachability rewards  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f327ff75e9 
								
							
								 
							
						 
						
							
							
								
								showing progress for bisimulation  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								74eeaa7f81 
								
							
								 
							
						 
						
							
							
								
								computing unbounded until on MDPs with the sparse helper now respects solver requirements  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								569b0122b8 
								
							
								 
							
						 
						
							
							
								
								introduced different minmax equation system types for requirement retrieval  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f7c803827b 
								
							
								 
							
						 
						
							
							
								
								remove debug output  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4adee85fa5 
								
							
								 
							
						 
						
							
							
								
								added checking requirements of MinMax solvers to model checker helpers  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3829b58e0d 
								
							
								 
							
						 
						
							
							
								
								introduced top-level solve equations function to centrally check for requirements  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								72234e96b2 
								
							
								 
							
						 
						
							
							
								
								started on requirements for MinMax solvers  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3c8f9a2ecf 
								
							
								 
							
						 
						
							
							
								
								Added 5th build stage  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e278c3ef69 
								
							
								 
							
						 
						
							
							
								
								moving from internal reference to pointer in StandardMinMax solver  
							
							
 
							
							
							equipped MinMax solvers with default constructors 
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								0c5aa1645d 
								
							
								 
							
						 
						
							
							
								
								fix reward model generation in JIT builder  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5bb6564078 
								
							
								 
							
						 
						
							
							
								
								remove debug output  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								06ec288296 
								
							
								 
							
						 
						
							
							
								
								enabled pcaa test that uses rational numbers  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								2d2cc95774 
								
							
								 
							
						 
						
							
							
								
								fixed issue  #12  raised by Joachim Klein  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								beb80cc5af 
								
							
								 
							
						 
						
							
							
								
								fixes issue  #11  raised by Joachim Klein  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								2d30108b49 
								
							
								 
							
						 
						
							
							
								
								fixes issue  #10  raised by Joachim Klein  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ecade3f857 
								
							
								 
							
						 
						
							
							
								
								fixes issue  #9  raised by Joachim Klein  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								12c79ad6ea 
								
							
								 
							
						 
						
							
							
								
								export choice labels  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e2e1407f3e 
								
							
								 
							
						 
						
							
							
								
								not calling sylvan_var on leaf nodes of sylvan anymore  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5856d9fe51 
								
							
								 
							
						 
						
							
							
								
								removed some debug output  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								04a24a2108 
								
							
								 
							
						 
						
							
							
								
								Merge remote-tracking branch 'origin/master' into symbolic_bisimulation  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6bebb3c9d5 
								
							
								 
							
						 
						
							
							
								
								fix bug in rational number/function handling with sylvan  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ee87067c9a 
								
							
								 
							
						 
						
							
							
								
								fixed type to make gcc happy  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d2a493a92d 
								
							
								 
							
						 
						
							
							
								
								fixed several crucial bugs related to dd bisimulation, tests now passing  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a7dcdcd84d 
								
							
								 
							
						 
						
							
							
								
								started on tests and added a ton of debug output  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								11d2ee2fda 
								
							
								 
							
						 
						
							
							
								
								making sure to add meta variables to transition matrix DD to make sure one can abstract from them later  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								36554b5b87 
								
							
								 
							
						 
						
							
							
								
								fixed some issues with reward preservation in dd-based bisimulation  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9a6abf7eec 
								
							
								 
							
						 
						
							
							
								
								fixed a bug in dd-based reward model building  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b120b74fa9 
								
							
								 
							
						 
						
							
							
								
								StateActionPair to index should be part of nondeterministicmodel  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6e506e5a66 
								
							
								 
							
						 
						
							
							
								
								moved application of permissive scheduler to an own transformer  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d271824461 
								
							
								 
							
						 
						
							
							
								
								prepare to initialize but not make settings known, not yet fully functioning  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d2002129b7 
								
							
								 
							
						 
						
							
							
								
								remove output  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e0452be54b 
								
							
								 
							
						 
						
							
							
								
								move some of the cli stuff to an own header  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								40a982430c 
								
							
								 
							
						 
						
							
							
								
								cmake for carl: handle situation where carl version information is missing  
							
							
 
							
							
							Older carl versions don't provide detailed version information, so we
provide an informative error message instead of cmake syntax errors during
the comparison. 
							
						 
						8 years ago