45486600f7 
								
							
								 
							
						 
						
							
							
								
								Made parts of the interface of the DdManager protected (because they shouldn't be accessible from the outside world).  
							
							
 
							
							
							Former-commit-id: bf52a653b8 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								389fddc996 
								
							
								 
							
						 
						
							
							
								
								Added some more methods to valuations. Changed visitor invocation slightly. Moves ExpressionReturnType in separate file. Finished linearity checking visitor. Started on visitor that extracts coefficients of linear expressions.  
							
							
 
							
							
							Former-commit-id: 6e3d0ec910 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								57a8381f91 
								
							
								 
							
						 
						
							
							
								
								If requested, the DD iterator can now skip meta variables which are 'don't cares' for the function value.  
							
							
 
							
							
							Former-commit-id: 061cb5f0fa 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								db232fe39b 
								
							
								 
							
						 
						
							
							
								
								Moved from pair to MatrixEntry as the basic building block of the matrix. Now matrix elements can be accessed in a more readable way.  
							
							
 
							
							
							Former-commit-id: f6514eb0cd 
							
						 
						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  
				
					
						
							
							
								 
						
							
							
							
								
							
								8d3ed7d2fa 
								
							
								 
							
						 
						
							
							
								
								Added min/max functions on DDs. Added tests for them and ite operation.  
							
							
 
							
							
							Former-commit-id: 8e6df90a38 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6078e07476 
								
							
								 
							
						 
						
							
							
								
								First version of DD iterator; small test included.  
							
							
 
							
							
							Former-commit-id: 2ec2323886 
							
						 
						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  
				
					
						
							
							
								 
						
							
							
							
								
							
								311247ff0c 
								
							
								 
							
						 
						
							
							
								
								Added support for Xor in expression classes and added parsing functionality for Xor, Implies and Iff.  
							
							
 
							
							
							Former-commit-id: 16e023cf26 
							
						 
						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  
				
					
						
							
							
								 
						
							
							
							
								
							
								94b25c02ca 
								
							
								 
							
						 
						
							
							
								
								Fixed bugs in some files.  
							
							
 
							
							
							Made LTL a little better to compile under WIN32.
Former-commit-id: 71377f0672 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								164c8225fd 
								
							
								 
							
						 
						
							
							
								
								Fixed some minor issues.  
							
							
 
							
							
							Former-commit-id: 80f0ae4c9c 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								199b6576a9 
								
							
								 
							
						 
						
							
							
								
								Added ternary operator. Parsing standard PRISM models into the PRISM classes now works. Included tests for parsing stuff. ToDo: add remaining semantic checks for parsing/PRISM classes and fix explicit model adapter.  
							
							
 
							
							
							Former-commit-id: cb37c98f1f 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								eb2b2fed30 
								
							
								 
							
						 
						
							
							
								
								Hotfix for DD abstraction layer: copy and paste mistake in operator !\= is now fixed.  
							
							
 
							
							
							Former-commit-id: b815b7d7e8 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								41b31df0ab 
								
							
								 
							
						 
						
							
							
								
								Added small tests for implies/iff in expressions.  
							
							
 
							
							
							Former-commit-id: 3d90be7596 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6e1241211b 
								
							
								 
							
						 
						
							
							
								
								Started moving IR and adjusting it to the new expression classes.  
							
							
 
							
							
							Former-commit-id: 24a182701f 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								8af52c8866 
								
							
								 
							
						 
						
							
							
								
								Finished new expression classes and corresponding functional tests.  
							
							
 
							
							
							Former-commit-id: 9268eab3a9 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c8a8beca2a 
								
							
								 
							
						 
						
							
							
								
								Started working on new easy-to-use expression classes.  
							
							
 
							
							
							Former-commit-id: 9ee1be5822 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								88d9f36ef4 
								
							
								 
							
						 
						
							
							
								
								Added min/max abstract over DD variables to CUDD (actual code taken from PRISM). Added more tests for DD layer. Fixed some bugs in the DD layer.  
							
							
 
							
							
							Former-commit-id: a4b7810137 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								0fce0444f7 
								
							
								 
							
						 
						
							
							
								
								Further bugfixes and tests for DD layer.  
							
							
 
							
							
							Former-commit-id: 32ef63f9b1 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								cf5c04065e 
								
							
								 
							
						 
						
							
							
								
								Added streaming functionality to DD. More tests, more bugfixes.  
							
							
 
							
							
							Former-commit-id: 3c3078fbdc 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6b07643c96 
								
							
								 
							
						 
						
							
							
								
								Further tests for DD layer and bugfixing.  
							
							
 
							
							
							Former-commit-id: 752a8c55ac 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a4fec9f080 
								
							
								 
							
						 
						
							
							
								
								Started writing functional tests for DD abstraction layer and fixed some bugs on the way.  
							
							
 
							
							
							Former-commit-id: 8a2fc118be 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								12743e0a7e 
								
							
								 
							
						 
						
							
							
								
								Moved from additional row grouping to the one embedded in the matrix itself.  
							
							
 
							
							
							Former-commit-id: 9d7a1fff10 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d70bb836bb 
								
							
								 
							
						 
						
							
							
								
								Tests are now working again with the row-grouped matrix.  
							
							
 
							
							
							Former-commit-id: b58e76b5bb 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								38833e308f 
								
							
								 
							
						 
						
							
							
								
								Started to add row-grouping to sparse matrix class.  
							
							
 
							
							
							Former-commit-id: 39e3703095 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								98b0bcf187 
								
							
								 
							
						 
						
							
							
								
								Reimplemented the TopologicalValueIterationNondeterministicLinearEquationSolver with splitting into submatrices.  
							
							
 
							
							
							Added a dtmc example for tests with the StronglyConnectedComponentDecomposition.
Former-commit-id: 0c33793fe6 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								15d13bc06d 
								
							
								 
							
						 
						
							
							
								
								Refactored the AutoParser.  
							
							
 
							
							
							- Devided the AutoParser.h into .h and .cpp
- The AutoParser now is a stateless class
|- This resulted in changes to the interface between the parsers and the rest of the project.
|- The main() now directly acquires a shared_ptr to an AbstractModel from the call of the AutoParser and keeps ownership of it.
|- Additionally, the division into .h and .cpp lead to a move of includes from the header to the source. This caused several tests to need some model header to be included.
|- Tests are still showing green (except those needing Gurobi, which I do not have).
Next up: Parser.h/.cpp, then comments and making things look nice.)
Former-commit-id: f59b7405e5 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								efb244a447 
								
							
								 
							
						 
						
							
							
								
								Added functional tests for scheduler classes.  
							
							
 
							
							
							Former-commit-id: d7f7da5ab0 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f79329bd9d 
								
							
								 
							
						 
						
							
							
								
								Fixed SCC decomposition. Added functional tests for SCC decomposition.  
							
							
 
							
							
							Former-commit-id: 25a7805fcb 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e80bb0caa5 
								
							
								 
							
						 
						
							
							
								
								Added functional tests for MEC decomposition.  
							
							
 
							
							
							Former-commit-id: 66b1265ebb 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								35d16a1191 
								
							
								 
							
						 
						
							
							
								
								Replaced VectorSet bei boost::container::flat_set, which does essentially the same. Fixed a bug in sparse matrix creation.  
							
							
 
							
							
							Former-commit-id: cb632bcfd4 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f684ce7799 
								
							
								 
							
						 
						
							
							
								
								Removed obsolete constructors of sparse matrix class as the new matrix builder is supposed to be used anyway. Fixed some minor issues.  
							
							
 
							
							
							Former-commit-id: ee8a7cc440 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								81cf0e2b22 
								
							
								 
							
						 
						
							
							
								
								Added SparseMatrixBuilder class that actually builds the matrices. A call to build() will then generate the matrix. This eliminates superfluous checks in the matrix that slowed down performance.  
							
							
 
							
							
							Former-commit-id: af5d946fb8 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								cf2b84b281 
								
							
								 
							
						 
						
							
							
								
								Further work on iterators for sparse matrix.  
							
							
 
							
							
							Former-commit-id: 8e78262161 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e08b61b9f7 
								
							
								 
							
						 
						
							
							
								
								Added functional and performance tests for sparse matrix.  
							
							
 
							
							
							Former-commit-id: dd9abe1826 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a26f63be30 
								
							
								 
							
						 
						
							
							
								
								Finished reworking the sparse matrix implementation. Adapted all other classes to the (partially) new API of the matrix.  
							
							
 
							
							
							Former-commit-id: 2c3b5a5bc3 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d5cadc0f4b 
								
							
								 
							
						 
						
							
							
								
								Finalized interface of bit vector. Added unit tests for all methods of the bit vector.  
							
							
 
							
							
							Former-commit-id: 6c7834ed20 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								07fbff7a07 
								
							
								 
							
						 
						
							
							
								
								Started refactoring bit vector class.  
							
							
 
							
							
							Former-commit-id: a2fecfce2b 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								158430418e 
								
							
								 
							
						 
						
							
							
								
								Replaced boost integer mask includes with cstdint  
							
							
 
							
							
							Reimplemented Gmm conversion with in place constructors
Former-commit-id: 003f582f9c 
							
						 
						12 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								42b9072cbf 
								
							
								 
							
						 
						
							
							
								
								Implemented TBB Parallelization Support into SparseMatrix.h  
							
							
 
							
							
							Re-factored Includes in CMake for TBB
Former-commit-id: b5ebf4153a 
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ec91dcbe2e 
								
							
								 
							
						 
						
							
							
								
								Merge branch master into LTLParser  
							
							
								
 
							
							
						 
						13 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								27de566228 
								
							
								 
							
						 
						
							
							
								
								Moved current tests to the functional test suite in an attempt to introduce performance tests.  
							
							
								
 
							
							
						 
						13 years ago