98f87a5e6d 
								
							
								 
							
						 
						
							
							
								
								Adapted Z3ExpressionAdapter for new expressions  
							
							
 
							
							
							SmtSolver now not copyable
Former-commit-id: e0d17fd21c 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a0df98a6eb 
								
							
								 
							
						 
						
							
							
								
								Removed unnecessary virtual keyword in Expression class.  
							
							
 
							
							
							Former-commit-id: f879cd579e 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								219af9b43b 
								
							
								 
							
						 
						
							
							
								
								Removed constants from expressions. Even though PRISM has the concept of constants and variables, it currently makes no sense to distinguish them in our expression classes.  
							
							
 
							
							
							Former-commit-id: 787e921e2c 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c6976dd8b5 
								
							
								 
							
						 
						
							
							
								
								Added some query methods for new expression classes.  
							
							
 
							
							
							Former-commit-id: 0633c7740e 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4cb346f8ce 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' into SmtSolvers  
							
							
 
							
							
							Former-commit-id: 7fca03c3ab 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d00cf794f1 
								
							
								 
							
						 
						
							
							
								
								Fixed wrong invocation of option system so all tests pass again, sorry about that, Philipp. :)  
							
							
 
							
							
							Former-commit-id: 475923edc4 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9b31033d05 
								
							
								 
							
						 
						
							
							
								
								Added options for Cudd manager to set precision, reordering technique and maxmem.  
							
							
 
							
							
							Former-commit-id: c18bfab518 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f69b79593c 
								
							
								 
							
						 
						
							
							
								
								initial interface for smt solver wrappers  
							
							
 
							
							
							Former-commit-id: e43b7afb3c 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3667261429 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' into PrismParserErrorHandling  
							
							
 
							
							
							Former-commit-id: 5f7743942c 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c76e0e8d4d 
								
							
								 
							
						 
						
							
							
								
								Added class for initial construct of PRISM programs (to capture position information). Added more validity checks for programs and tests for them (not all though).  
							
							
 
							
							
							Former-commit-id: cf4e985684 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								83f9832e2d 
								
							
								 
							
						 
						
							
							
								
								Added type check visitor to validate types of identifiers in expressions. Started writing validation method on PRISM program class.  
							
							
 
							
							
							Former-commit-id: 6416bea711 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								873d80cd2d 
								
							
								 
							
						 
						
							
							
								
								If a module is renamed from some other module, this is now kept track of in the respective PRISM classes.  
							
							
 
							
							
							Former-commit-id: c07e25ac55 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								82836f1ad1 
								
							
								 
							
						 
						
							
							
								
								Added some checks for validity of identifiers in PRISM programs. Added some illegal tests to test suite.  
							
							
 
							
							
							Former-commit-id: fc44db75a7 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6f9dd7107d 
								
							
								 
							
						 
						
							
							
								
								Added universal abstraction function to DD layer.  
							
							
 
							
							
							Former-commit-id: 56e5d62b5a 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d0d80cf5e1 
								
							
								 
							
						 
						
							
							
								
								Started on making the PrismParser more robust.  
							
							
 
							
							
							Former-commit-id: 7ce1351d0c 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								2f5f8c0918 
								
							
								 
							
						 
						
							
							
								
								PrctlFilter is operational but not yet complete (proper standard output missing).  
							
							
 
							
							
							- General function of the filters: The filter as an abstraction layer between the control flow and the formula/modelchecker.
|- It has a formula as child but is not a formula itself.
|- It invokes the modelchecking process on the child formula and manipulates the result.
|- For the purpose of result manipulation it keeps a list of filter actions.
|- Each action manipulates the result in a certain way. For example: It returns only the results for states 25 to 140.
|- Furthermore the printing of the result to standard out and the log is no longer done by the modelchecker but by the filter.
|- That way the tasks of each class becomes more clear: Modelchecker to compute the results, filter to prepare the computed results for write out.
- Battled with a major design problem: How to integrate the optimizing operator (aka. min or max probs for non-det. models) into the filter scheme.
|- It is now integrated as a separate filter action, which does not touch the results but hold the flag determining whether to maximize or to minimize.
|- This action must be the innermost filter action (i.e. the first list entry) to have any effect.
|- This is combined with a special fuction of the modelchecker that manipulates the mutable minimizationStack calculates the modelchecking result and resets the stack to its original state.
|- This way the information whether to min, to max or not to try is managed by the filter and propagated as needed.
|- Remark: Fixed a major risk of undefined behavior in the SparseMdpPrctlModelChecker.
   |- If the formula to be checked did not have a NoBoundFormula as root then the minimumOperatorStack would be empty and minimumOperatorStack.top() would result in undefined behavior.
   |- Added tests whether the stack is empty before trying to read out the possibly non existant top element.
Next up: Implement similar filters for LTL and CSL and try to get it compiled.
Former-commit-id: 577998e027 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3d41c36153 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' into parametricSystems  
							
							
 
							
							
							Former-commit-id: f6752d5c26 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5816bd8860 
								
							
								 
							
						 
						
							
							
								
								Bugfix for explicit model adapter: empty choice labeling was not created for automatically added self-loops.  
							
							
 
							
							
							Former-commit-id: 6c63c28f59 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6bc50e3d76 
								
							
								 
							
						 
						
							
							
								
								brp example  
							
							
 
							
							
							Former-commit-id: 06d1553d5f 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								72c804815e 
								
							
								 
							
						 
						
							
							
								
								several *small* fixes and better direct encoding  
							
							
 
							
							
							Former-commit-id: 04265d8fb5 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								299390cef5 
								
							
								 
							
						 
						
							
							
								
								Started on the filters.  
							
							
 
							
							
							- Got the general structure down.
- Now writing the output functions.
Next up: Finish the basic filter functionality.
Former-commit-id: 91daa0a9f7 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								44ba492fe7 
								
							
								 
							
						 
						
							
							
								
								CuddDdManager now sets tolerance to 1e-15.  
							
							
 
							
							
							Former-commit-id: bfc985b5de 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c0b5757e4d 
								
							
								 
							
						 
						
							
							
								
								Adding new atomic propositions and attach it to a set of states  
							
							
 
							
							
							Former-commit-id: 2fee551b17 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								8d3ed7d2fa 
								
							
								 
							
						 
						
							
							
								
								Added min/max functions on DDs. Added tests for them and ite operation.  
							
							
 
							
							
							Former-commit-id: 8e6df90a38 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3387e288f8 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' into parametricSystems  
							
							
 
							
							
							Former-commit-id: 0c71b31069 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d4c2657856 
								
							
								 
							
						 
						
							
							
								
								Parsing parameteric dtmcs and exporting them to smt2  
							
							
 
							
							
							Former-commit-id: c791625d40 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5b06259a05 
								
							
								 
							
						 
						
							
							
								
								Added ite operator for DDs in abstraction layer.  
							
							
 
							
							
							Former-commit-id: b1bc85e9e3 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3eb8f8e328 
								
							
								 
							
						 
						
							
							
								
								Bugfix: valuations now correctly store the given initial value for boolean variables.  
							
							
 
							
							
							Former-commit-id: a23f014303 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								39ec9401ef 
								
							
								 
							
						 
						
							
							
								
								Fixed the PrismParser so the exact format of PRISMs boolean expressions can now be parsed.  
							
							
 
							
							
							Former-commit-id: bb08ec1646 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								63601e0b8a 
								
							
								 
							
						 
						
							
							
								
								Calling getExpression on an undefined constant is now properly treated with an exception.  
							
							
 
							
							
							Former-commit-id: 2d3e06a20a 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f1cac96d4c 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' of  https://sselab.de/lab9/private/git/storm  
							
							
 
							
							
							Former-commit-id: f784694298 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								dc80b987c2 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' into ddLayerExtensions  
							
							
 
							
							
							Former-commit-id: 9eab593479 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6078e07476 
								
							
								 
							
						 
						
							
							
								
								First version of DD iterator; small test included.  
							
							
 
							
							
							Former-commit-id: 2ec2323886 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f2383ccfb5 
								
							
								 
							
						 
						
							
							
								
								Added missing definitions required for CUDD to compile under 64bit architectures.  
							
							
 
							
							
							Former-commit-id: 4e40ea7ee3 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								0a501b6e76 
								
							
								 
							
						 
						
							
							
								
								Added a constructor for GlobalProgramInformation as MSVC fails to default bool to false.  
							
							
 
							
							
							Former-commit-id: bd50a770c8 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								90fc5faca2 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' of  https://sselab.de/lab9/private/git/storm  
							
							
 
							
							
							Former-commit-id: 6bae9c23cf 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1d8ae9fc89 
								
							
								 
							
						 
						
							
							
								
								Fixed an issue with templated variadic template arguments (see  http://stackoverflow.com/questions/23119273/use-a-templated-variadic-template-parameter-as-specialized-parameter  for discussion)  
							
							
 
							
							
							Former-commit-id: e7d2d054b6 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d57a0c9901 
								
							
								 
							
						 
						
							
							
								
								Replaced memcpy by std::copy.  
							
							
 
							
							
							Former-commit-id: ef31cf9977 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								311247ff0c 
								
							
								 
							
						 
						
							
							
								
								Added support for Xor in expression classes and added parsing functionality for Xor, Implies and Iff.  
							
							
 
							
							
							Former-commit-id: 16e023cf26 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3940dbf45c 
								
							
								 
							
						 
						
							
							
								
								Accessing index of node via method interface, not member access.  
							
							
 
							
							
							Former-commit-id: d53006d5d4 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5fe7ffe51a 
								
							
								 
							
						 
						
							
							
								
								Added missing function declaration in CUDD'c C++ interface. Started on an iterator for DD valuations.  
							
							
 
							
							
							Former-commit-id: a97ccdec3d 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								7ca6a4edeb 
								
							
								 
							
						 
						
							
							
								
								sub part for parameters, working parsing for non parametric systems into a parametric system  
							
							
 
							
							
							Former-commit-id: 7714692e32 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								8142a8e004 
								
							
								 
							
						 
						
							
							
								
								some fixes for using something different from doubles for templated value type :)  
							
							
 
							
							
							Former-commit-id: d26d06b265 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f9a0c94c1b 
								
							
								 
							
						 
						
							
							
								
								added options for encoded reachability and parameters  
							
							
 
							
							
							Former-commit-id: 7456b4c0a3 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								61d4bb956c 
								
							
								 
							
						 
						
							
							
								
								Added functionality to compare two ADDs up to a given precision. Added logical operator overloads to DD interface. Added tests for all new features.  
							
							
 
							
							
							Former-commit-id: 738ad49d62 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5a4730ae22 
								
							
								 
							
						 
						
							
							
								
								When exporting DDs to the dot format, edges leading to the zero node are now suppressed. Also, nodes in the dot file are now labeled with variable names (+ the number of the bit).  
							
							
 
							
							
							Former-commit-id: 410d61d333 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6025dce144 
								
							
								 
							
						 
						
							
							
								
								Further work on the formuolas.  
							
							
 
							
							
							- Finished the third and last logic: Csl.
- Note that nothing compiles as of yet. This is due to the removal of the NoBoundOperators wich are expected to be replaced by filters.
Former-commit-id: d26ae768f7 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								94b25c02ca 
								
							
								 
							
						 
						
							
							
								
								Fixed bugs in some files.  
							
							
 
							
							
							Made LTL a little better to compile under WIN32.
Former-commit-id: 71377f0672 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								dc8921037e 
								
							
								 
							
						 
						
							
							
								
								Added missing test inputs.  
							
							
 
							
							
							Former-commit-id: 537971f365 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b654866cb2 
								
							
								 
							
						 
						
							
							
								
								Merge branch 'master' into param_dtmc2smt  
							
							
 
							
							
							Former-commit-id: 7eb2effb2f 
							
						 
						12 years ago