Alexander Bork
							
						 | 
						
							
							
							
								
							
								5765824782
								
							
								
							
						 | 
						
							
							
								
								Reworked SMT result interface
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Alexander Bork
							
						 | 
						
							
							
							
								
							
								38ccd51ae1
								
							
								
							
						 | 
						
							
							
								
								Added check for conflicts between dependencies in the DFT
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Alexander Bork
							
						 | 
						
							
							
							
								
							
								80fc8fb56b
								
							
								
							
						 | 
						
							
							
								
								Fix for error that checkbound may be large than number of Markovian states
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Matthias Volk
							
						 | 
						
							
							
							
								
							
								0070b7762a
								
							
								
							
						 | 
						
							
							
								
								Merge branch 'master' into dft_iso
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Matthias Volk
							
						 | 
						
							
							
							
								
							
								9ebd1af737
								
							
								
							
						 | 
						
							
							
								
								Removed unused method again
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Matthias Volk
							
						 | 
						
							
							
							
								
							
								65a310dc8b
								
							
								
							
						 | 
						
							
							
								
								Test for allUntilProbabilities
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								TimQu
							
						 | 
						
							
							
							
								
							
								c27e542bf1
								
							
								
							
						 | 
						
							
							
								
								Merge branch 'master' into deterministicScheds
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								TimQu
							
						 | 
						
							
							
							
								
							
								fcb5f094dc
								
							
								
							
						 | 
						
							
							
								
								Fixed a tybo.
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								TimQu
							
						 | 
						
							
							
							
								
							
								0eda4b4041
								
							
								
							
						 | 
						
							
							
								
								DeterministicSchedsLpChecker: Started to treat End Components properly.
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Jip Spel
							
						 | 
						
							
							
							
								
							
								4825cb254f
								
							
								
							
						 | 
						
							
							
								
								Precision as argument
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								TimQu
							
						 | 
						
							
							
							
								
							
								621aae1c4c
								
							
								
							
						 | 
						
							
							
								
								DeterministicSchedsParetoExplorer: Selecting LP-based weight vector checkers in case of properties that are not supported by the standard weight vector checker.
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Jip Spel
							
						 | 
						
							
							
							
								
							
								1557f6d213
								
							
								
							
						 | 
						
							
							
								
								Use precision in sample checking monotonicity
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Jip Spel
							
						 | 
						
							
							
							
								
							
								8732a7f40d
								
							
								
							
						 | 
						
							
							
								
								Make variabletype depend on value type
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Jip Spel
							
						 | 
						
							
							
							
								
							
								7f5416adb8
								
							
								
							
						 | 
						
							
							
								
								Clean up LatticeExtender
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Jip Spel
							
						 | 
						
							
							
							
								
							
								c0aa6eefa3
								
							
								
							
						 | 
						
							
							
								
								Clean up Lattice
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Jip Spel
							
						 | 
						
							
							
							
								
							
								fa97e0138f
								
							
								
							
						 | 
						
							
							
								
								Clean up assumption maker
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Jip Spel
							
						 | 
						
							
							
							
								
							
								ee08139641
								
							
								
							
						 | 
						
							
							
								
								Fix test
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Jip Spel
							
						 | 
						
							
							
							
								
							
								3ebd5f0bf6
								
							
								
							
						 | 
						
							
							
								
								Clean up assumption checker
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Jip Spel
							
						 | 
						
							
							
							
								
							
								0d1ddb6232
								
							
								
							
						 | 
						
							
							
								
								Make sampling in monotonicity-analysis optional
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Jip Spel
							
						 | 
						
							
							
							
								
							
								77a70179d3
								
							
								
							
						 | 
						
							
							
								
								Update MonotonicityChecker
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								TimQu
							
						 | 
						
							
							
							
								
							
								1a4fe91797
								
							
								
							
						 | 
						
							
							
								
								Removed unused files.
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Matthias Volk
							
						 | 
						
							
							
							
								
							
								c361d59d65
								
							
								
							
						 | 
						
							
							
								
								Merge branch 'master' into dft_iso
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Alexander Bork
							
						 | 
						
							
							
							
								
							
								28a878f154
								
							
								
							
						 | 
						
							
							
								
								Adjusted lower bound correction to new BE distinction
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								TimQu
							
						 | 
						
							
							
							
								
							
								18f0c3d125
								
							
								
							
						 | 
						
							
							
								
								MemoryIncorporation: improved documentation.
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								TimQu
							
						 | 
						
							
							
							
								
							
								6d67a3671b
								
							
								
							
						 | 
						
							
							
								
								Merge branch 'master' into deterministicScheds
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								TimQu
							
						 | 
						
							
							
							
								
							
								f9b06e7eaf
								
							
								
							
						 | 
						
							
							
								
								Updated changelog.
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								TimQu
							
						 | 
						
							
							
							
								
							
								70b9398b90
								
							
								
							
						 | 
						
							
							
								
								storage/Scheduler: Fixed a constructor.
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Matthias Volk
							
						 | 
						
							
							
							
								
							
								7995100441
								
							
								
							
						 | 
						
							
							
								
								Small fixes in DFT tests
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Matthias Volk
							
						 | 
						
							
							
							
								
							
								521461737a
								
							
								
							
						 | 
						
							
							
								
								Adaption to changes in BEs
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Matthias Volk
							
						 | 
						
							
							
							
								
							
								23f1e73137
								
							
								
							
						 | 
						
							
							
								
								Merge from branch 'dft'
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Tim Quatmann
							
						 | 
						
							
							
							
								
							
								5380d9c050
								
							
								
							
						 | 
						
							
							
								
								Merge branch 'master' into deterministicScheds
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Tim Quatmann
							
						 | 
						
							
							
							
								
							
								63a9b4485b
								
							
								
							
						 | 
						
							
							
								
								FormulaParserGrammar: Adding support for time-bounded formulas with exact time-bound, e.g., F=12 "target"
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Alexander Bork
							
						 | 
						
							
							
							
								
							
								f37bcea1ea
								
							
								
							
						 | 
						
							
							
								
								Added test for bound correction
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Jip Spel
							
						 | 
						
							
							
							
								
							
								73a514a9c7
								
							
								
							
						 | 
						
							
							
								
								Fix validation of assumptions/use it
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Tim Quatmann
							
						 | 
						
							
							
							
								
							
								b4f652bbc8
								
							
								
							
						 | 
						
							
							
								
								Reducing the nesting when creating a expression::sum(...).
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Tim Quatmann
							
						 | 
						
							
							
							
								
							
								a829c52a0d
								
							
								
							
						 | 
						
							
							
								
								ExpressionParser can now parse round expressions.
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Tim Quatmann
							
						 | 
						
							
							
							
								
							
								66a7bd5954
								
							
								
							
						 | 
						
							
							
								
								implemented creation of round expression.
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Tim Quatmann
							
						 | 
						
							
							
							
								
							
								b70f28b10e
								
							
								
							
						 | 
						
							
							
								
								Ensured that utility function for rounding always rounds towards infinity.
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Tim Quatmann
							
						 | 
						
							
							
							
								
							
								0e18046934
								
							
								
							
						 | 
						
							
							
								
								Fixed translating ceil(x) to mathsat expressions.
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Tim Quatmann
							
						 | 
						
							
							
							
								
							
								d201580d92
								
							
								
							
						 | 
						
							
							
								
								Refactored simplification of UnaryNumericalFunctionExpression.
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Tim Quatmann
							
						 | 
						
							
							
							
								
							
								a34037bff4
								
							
								
							
						 | 
						
							
							
								
								Added utility function for rounding.
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Alexander Bork
							
						 | 
						
							
							
							
								
							
								d42dea79c3
								
							
								
							
						 | 
						
							
							
								
								Added comments to explain the query
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Alexander Bork
							
						 | 
						
							
							
							
								
							
								74d1bf3c7e
								
							
								
							
						 | 
						
							
							
								
								Merge remote-tracking branch 'origin/dftSMT' into dftSMT
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Alexander Bork
							
						 | 
						
							
							
							
								
							
								948485c226
								
							
								
							
						 | 
						
							
							
								
								Reworked lower bound computation
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Alexander Bork
							
						 | 
						
							
							
							
								
							
								eeccb2092a
								
							
								
							
						 | 
						
							
							
								
								Added variables for trigger and resolution timepoints of dependencies
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Matthias Volk
							
						 | 
						
							
							
							
								
							
								426c293090
								
							
								
							
						 | 
						
							
							
								
								Travis: disable installation of carl-parser
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Matthias Volk
							
						 | 
						
							
							
							
								
							
								2d20365674
								
							
								
							
						 | 
						
							
							
								
								Travis: support for Ubuntu 19.04
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Matthias Volk
							
						 | 
						
							
							
							
								
							
								75cfa17966
								
							
								
							
						 | 
						
							
							
								
								Fixed compile issue on Linux
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Matthias Volk
							
						 | 
						
							
							
							
								
							
								5729066add
								
							
								
							
						 | 
						
							
							
								
								Merge branch 'master' into dft
							
							
							
							
								
							
							
						 | 
						7 years ago | 
					
				
					
						
							
							
								 
								Matthias Volk
							
						 | 
						
							
							
							
								
							
								a35735a630
								
							
								
							
						 | 
						
							
							
								
								Fixed computation of all until probabilities
							
							
							
							
								
							
							
						 | 
						7 years ago |