652aeb7562 
								
							
								 
							
						 
						
							
							
								
								Fixed compile error with CarlRationalNumber instead of RationalNumber  
							
							
 
							
							
							Former-commit-id: 0fbb4ad1c1 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6e8602413e 
								
							
								 
							
						 
						
							
							
								
								ModelInstantiator + test  
							
							
 
							
							
							Former-commit-id: f3c9980067 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								0b98412bb4 
								
							
								 
							
						 
						
							
							
								
								further work on making row-grouping optional  
							
							
 
							
							
							Former-commit-id: bae568660f 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f8b9ece2fd 
								
							
								 
							
						 
						
							
							
								
								Added mini test for BitVector  
							
							
 
							
							
							Former-commit-id: 8ec7395c0d 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								fad28df7d6 
								
							
								 
							
						 
						
							
							
								
								first working version of next-state generator for PRISM models  
							
							
 
							
							
							Former-commit-id: 548a725e25 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								da0dafe5be 
								
							
								 
							
						 
						
							
							
								
								ModelInstantiator!!!!11  
							
							
 
							
							
							Also: some refactoring
Former-commit-id: 663cd8e241 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6818c6dc0d 
								
							
								 
							
						 
						
							
							
								
								Fixed tests when no log4plus is available.  
							
							
 
							
							
							Former-commit-id: f1ae81376c 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5ce72a85ce 
								
							
								 
							
						 
						
							
							
								
								added small test for conditional probability and conditional rewards  
							
							
 
							
							
							Former-commit-id: 891d99eea6 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e40cc65117 
								
							
								 
							
						 
						
							
							
								
								added tests for fragment checker  
							
							
 
							
							
							Former-commit-id: 2de76ee5a5 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								dc8a5b11e0 
								
							
								 
							
						 
						
							
							
								
								more refactoring regarding fragment checking  
							
							
 
							
							
							Former-commit-id: fd335f6f8e 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3727018ef4 
								
							
								 
							
						 
						
							
							
								
								added functionality to sparse MDP helper to compute until probabilities just for maybe states (and produce the corresponding scheduler)  
							
							
 
							
							
							Former-commit-id: 79aae02a13 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								8f087597cc 
								
							
								 
							
						 
						
							
							
								
								more work towards proper scheduler generation  
							
							
 
							
							
							Former-commit-id: ee6237ef49 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5a1039838f 
								
							
								 
							
						 
						
							
							
								
								made everything compile again and all tests passing  
							
							
 
							
							
							Former-commit-id: 65c66fb58f 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4367bdb378 
								
							
								 
							
						 
						
							
							
								
								properly introduced CheckTask in all model checkers and made it compile again (+ functional tests working)  
							
							
 
							
							
							Former-commit-id: d44db3c342 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d8191d8c6a 
								
							
								 
							
						 
						
							
							
								
								const formulae  
							
							
 
							
							
							Former-commit-id: 910d7ca539 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ad01dfa611 
								
							
								 
							
						 
						
							
							
								
								refactored bisimulation a bit (mainly the entry point as well as hidden some options)  
							
							
 
							
							
							Former-commit-id: 5405a14930 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f0f3e8cbb3 
								
							
								 
							
						 
						
							
							
								
								Fixed test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp when MathSAT support is unavailable.  
							
							
 
							
							
							Former-commit-id: c4b91a2ac5 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3ce8643d96 
								
							
								 
							
						 
						
							
							
								
								Added benchmarks  
							
							
 
							
							
							Former-commit-id: 6979a9aece 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								0f6e6e4da1 
								
							
								 
							
						 
						
							
							
								
								added feature to compute step-bounded until probabilities in parametric models  
							
							
 
							
							
							Former-commit-id: 172e87cb55 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1225b056f2 
								
							
								 
							
						 
						
							
							
								
								a little refactoring  
							
							
 
							
							
							Former-commit-id: 9af14c006c 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1e1400d68d 
								
							
								 
							
						 
						
							
							
								
								merge  
							
							
 
							
							
							Former-commit-id: eb9efc4bb2 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d0e15d1a4f 
								
							
								 
							
						 
						
							
							
								
								more work (and stuff, you know?)  
							
							
 
							
							
							Former-commit-id: ec9f6746b8 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								0708672a68 
								
							
								 
							
						 
						
							
							
								
								removed ite for ADDs as this operation should be formed with a BDD as the first argument. as a compensation, we provide a version of ite that takes a BDD and two ADDs and returns the corresponding ADD  
							
							
 
							
							
							Former-commit-id: 720dc3a9c4 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f8fc39870a 
								
							
								 
							
						 
						
							
							
								
								hybrid and symbolic model checkers working with sylvan  
							
							
 
							
							
							Former-commit-id: d01b92e328 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								7376eaf866 
								
							
								 
							
						 
						
							
							
								
								made symbolic MDP model checker tests work  
							
							
 
							
							
							Former-commit-id: e2e0d07a55 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								7f75db2790 
								
							
								 
							
						 
						
							
							
								
								ADD iterator working for sylvan. enabled more tests for sylvan. symbolic Dtmc model checker now working.  
							
							
 
							
							
							Former-commit-id: b11b2f7476 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f2a01afbdf 
								
							
								 
							
						 
						
							
							
								
								ODD-based stuff working for Sylvan. Almost all tests passing  
							
							
 
							
							
							Former-commit-id: a6eef37d37 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								36a6e9e76e 
								
							
								 
							
						 
						
							
							
								
								more work on sylvan ODD-related stuff  
							
							
 
							
							
							Former-commit-id: 142f57620a 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								50e7bbfe35 
								
							
								 
							
						 
						
							
							
								
								fixed a tests, all tests running again  
							
							
 
							
							
							Former-commit-id: b271ae5e84 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ebe9ccbb15 
								
							
								 
							
						 
						
							
							
								
								some work on DD stuff  
							
							
 
							
							
							Former-commit-id: 50ca51d264 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								8657fb0181 
								
							
								 
							
						 
						
							
							
								
								introduced relational product operations to prob0/1 algorithms (where possible)  
							
							
 
							
							
							Former-commit-id: 7fcd642030 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e43bdfaaaa 
								
							
								 
							
						 
						
							
							
								
								more work on the dd stuff *sigh*  
							
							
 
							
							
							Former-commit-id: df8e227336 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								fb4c103320 
								
							
								 
							
						 
						
							
							
								
								merged sylvan updates into the sylvan copy. made more tests work  
							
							
 
							
							
							Former-commit-id: 18023e03c2 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								91fb664910 
								
							
								 
							
						 
						
							
							
								
								Refactored a little and implemented functions for prophesy  
							
							
 
							
							
							Former-commit-id: a61f1eaff2 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								10996b4ab5 
								
							
								 
							
						 
						
							
							
								
								more work on sylvan  
							
							
 
							
							
							Former-commit-id: c1bfcd83ee 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								7ea0cb19b3 
								
							
								 
							
						 
						
							
							
								
								added some new functions to sylvan. isolated new code to make it easier to update sylvan to newer versions later  
							
							
 
							
							
							Former-commit-id: 6b489993a5 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								8eb3720f91 
								
							
								 
							
						 
						
							
							
								
								more work on sylvan integration  
							
							
 
							
							
							Former-commit-id: 1bd63e5373 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6c1a21c43f 
								
							
								 
							
						 
						
							
							
								
								added more functions in sylvan  
							
							
 
							
							
							Former-commit-id: f2e0c158a6 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								2c69232560 
								
							
								 
							
						 
						
							
							
								
								started cleaning ADD interface  
							
							
 
							
							
							Former-commit-id: f67fe7cf47 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								472851508c 
								
							
								 
							
						 
						
							
							
								
								changed return type of equal, notEqual, less, lessOrEqual, greater, greaterOrEqual to BDD since returning an ADD is logically not quite correct  
							
							
 
							
							
							Former-commit-id: 64bf8b0704 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								8194454621 
								
							
								 
							
						 
						
							
							
								
								more work on making sylvan mtbdds work  
							
							
 
							
							
							Former-commit-id: 98454b0ff4 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								99f096635f 
								
							
								 
							
						 
						
							
							
								
								started integrating sylvan  
							
							
 
							
							
							Former-commit-id: 2aec043047 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f7992f5aa7 
								
							
								 
							
						 
						
							
							
								
								Forgot adaptation of test...  
							
							
 
							
							
							Former-commit-id: 263da953bc 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b4a4a81bb1 
								
							
								 
							
						 
						
							
							
								
								Renamed, moved, added some benchmarks  
							
							
 
							
							
							Former-commit-id: 670448c26f 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a258d1ab48 
								
							
								 
							
						 
						
							
							
								
								restructured ODD to be independent of the DD library being used  
							
							
 
							
							
							Former-commit-id: 83f08ba203 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								19029cd905 
								
							
								 
							
						 
						
							
							
								
								functional tests compile and run again, yay!  
							
							
 
							
							
							Former-commit-id: 60d3ce16b9 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4a874a5a29 
								
							
								 
							
						 
						
							
							
								
								Added some benchmark models from param website  
							
							
 
							
							
							Fixed two bugs considering nonatomic subformulae and constant results
Qualitative modelchecking needs to be done when applying a policy!
Former-commit-id: bd88228214 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								bf450688b4 
								
							
								 
							
						 
						
							
							
								
								The variable pool of carl needs to be cleared after executing a test.  
							
							
 
							
							
							Sampling for mdps now uses the policy of the previous iteration as initial guess
Former-commit-id: 3b8b25f30f 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4e86ef2e47 
								
							
								 
							
						 
						
							
							
								
								moved CUDD-based DD implementation to own folder  
							
							
 
							
							
							Former-commit-id: a828f92518 
							
						 
						10 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1d49bc6dd0 
								
							
								 
							
						 
						
							
							
								
								extracting the bisimulation quotient for MDPs; tests for MDP bisimulation  
							
							
 
							
							
							Former-commit-id: 5613c653ba 
							
						 
						10 years ago