bae41009a2 
								
							
								 
							
						 
						
							
							
								
								LRA method for MAs can now be switched to LP-based method  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								77c0cdc0e3 
								
							
								 
							
						 
						
							
							
								
								added minmax method 'linearprogramming'  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								724e059083 
								
							
								 
							
						 
						
							
							
								
								Fixed parsing prism models with action rewards that refer to action labels introduced during module renaming.  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								bda9a797e8 
								
							
								 
							
						 
						
							
							
								
								fixed some issues in CUDD (fixes provided by Fabio Somenzi)  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								66e1cf8bd6 
								
							
								 
							
						 
						
							
							
								
								Add support for Fedora's z3 package.  
							
							
 
							
							
							Fedora installs the z3 headers in /usr/include/z3, which was not being
detected by CMake.
Signed-off-by: dehnert <dehnert@cs.rwth-aachen.de> 
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								aebe9fa3c3 
								
							
								 
							
						 
						
							
							
								
								LP-based long run average rewards for MDPs  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								2646097d8e 
								
							
								 
							
						 
						
							
							
								
								added virtual destructor for NextStateGenerator  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ad9008e0c1 
								
							
								 
							
						 
						
							
							
								
								fixing more warnings related to struct vs. class forward declarations  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c03c5fceb7 
								
							
								 
							
						 
						
							
							
								
								fixed warnings related to the mixed use of struct/class  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								234b590bdf 
								
							
								 
							
						 
						
							
							
								
								Fixed #include  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5b35927ecb 
								
							
								 
							
						 
						
							
							
								
								fix for some multi-objective queries  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c0d364cf1b 
								
							
								 
							
						 
						
							
							
								
								fixed a warning  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								241fc88077 
								
							
								 
							
						 
						
							
							
								
								multi-dimensional time bounds  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								defcd7d5d7 
								
							
								 
							
						 
						
							
							
								
								Multi-objective model checking: adapted data structures to allow more general objectives  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d35a5e4bdd 
								
							
								 
							
						 
						
							
							
								
								returning the time bound type from a timeBoundReference  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9207f4fbd8 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'memoryproductimprovements'  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e8e189723f 
								
							
								 
							
						 
						
							
							
								
								fixed applying memoryless schedulers  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5651b23771 
								
							
								 
							
						 
						
							
							
								
								fixing minor compiling issue  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6af15f3a0d 
								
							
								 
							
						 
						
							
							
								
								Memory Structure Product with custom reward model type  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a348f6ea8e 
								
							
								 
							
						 
						
							
							
								
								function to apply a given scheduler to a nondeterministic model  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								7bd9ef798f 
								
							
								 
							
						 
						
							
							
								
								returning the memory structure of a scheduler  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4251c9f525 
								
							
								 
							
						 
						
							
							
								
								added function to build a trivial memory structure  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4351be5512 
								
							
								 
							
						 
						
							
							
								
								Allowed building memory product with respect to a scheduler  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5bdbc00bcd 
								
							
								 
							
						 
						
							
							
								
								Changed carlConfig path for shipped carl  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								43642fef84 
								
							
								 
							
						 
						
							
							
								
								Improved product of model and memory structure: We can now enforce that certain states are considered reachable.  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9bccae9c5c 
								
							
								 
							
						 
						
							
							
								
								uint_fast64_t -> uint64_t  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								11b9c60515 
								
							
								 
							
						 
						
							
							
								
								Adapted fragment checker test to new multiobjective-fragment specification  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								29855e2853 
								
							
								 
							
						 
						
							
							
								
								added option to display information about exploration progress to both jit and explicit builder  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								040c1f0d4c 
								
							
								 
							
						 
						
							
							
								
								fixed ignoring the hypothesis when not doing refinement  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								48e029dd9d 
								
							
								 
							
						 
						
							
							
								
								Adapted region settings and CLI to new features.  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6621cb814c 
								
							
								 
							
						 
						
							
							
								
								new argument validator: doubleRangeValidatorIncluding  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								56616f1e26 
								
							
								 
							
						 
						
							
							
								
								trying to clarify sylvan dependency on carl  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								53a2723e0c 
								
							
								 
							
						 
						
							
							
								
								storm pars result moved from storm to storm pars  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5a3c67c352 
								
							
								 
							
						 
						
							
							
								
								Use result.toString to generate easier-to-parse result files  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3bcdc1b579 
								
							
								 
							
						 
						
							
							
								
								allowing to read transient variables in guards of edges in JIT-based JANI model builder and making the optimization level an option  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6fd75ac37e 
								
							
								 
							
						 
						
							
							
								
								fixed issue in cli related to transforming PRISM to JANI  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9591157996 
								
							
								 
							
						 
						
							
							
								
								new features for storm-pars api:  
							
							
 
							
							
							- depth limit for iterative refinement
- the regions with inconclusive result are now also part of the result
- when analyzing a region, a hypothesis (AllSat or AllViolated) can now be given 
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								8aa2b57640 
								
							
								 
							
						 
						
							
							
								
								minor fix for multi-objective preprocessor  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9bfb1fedc2 
								
							
								 
							
						 
						
							
							
								
								requiring that multi objective queries have a multi(..) formula at top level.  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								275f1ff15e 
								
							
								 
							
						 
						
							
							
								
								only filter the result if there actually is a result and a filter  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								0e88d711e8 
								
							
								 
							
						 
						
							
							
								
								Correctly handled reward bounded objectives in multi-objective preprocessing  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b44870dc09 
								
							
								 
							
						 
						
							
							
								
								implemented SMT-Lib export SmtSolver interface  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d6447a56f0 
								
							
								 
							
						 
						
							
							
								
								minor fixes for reward bounded formulas  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c1b4cb848c 
								
							
								 
							
						 
						
							
							
								
								added missing newlines in the storm-pars cli. Also do not segfault when there is no result  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								07259e8f0d 
								
							
								 
							
						 
						
							
							
								
								added parser for IMCAs explicit Markov automaton format  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1f71e9af79 
								
							
								 
							
						 
						
							
							
								
								extend debug output of gmmxx adapter  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5b868081f0 
								
							
								 
							
						 
						
							
							
								
								Fixed MA LRA computation for the case where the whole MA is a MEC  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								89d8993cfb 
								
							
								 
							
						 
						
							
							
								
								updated changelog (long-run rewards on MAs)  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c46ce03e60 
								
							
								 
							
						 
						
							
							
								
								make storm compile with latest version of carl  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4a43d7ab0d 
								
							
								 
							
						 
						
							
							
								
								towards compiling storm with the latest carl version  
							
							
								
 
							
							
						 
						8 years ago