|  Tim Quatmann | 7023736e3d | Added resource-gathering testfile | 5 years ago | 
				
					
						|  Tim Quatmann | ee06a1f1a6 | Also added test case for lra operator formula. | 5 years ago | 
				
					
						|  Tim Quatmann | 6154bd39f9 | Fixes for new test case. | 5 years ago | 
				
					
						|  Tim Quatmann | 3789fbb3e9 | Test case for multi-objective lra | 5 years ago | 
				
					
						|  TimQu | 07f7ce7963 | Merge branch 'master' into multi-objective-lra | 5 years ago | 
				
					
						|  TimQu | f100ff6275 | LraViHelper: Fixed unordered insertion into SparseMatrixBuilder. | 5 years ago | 
				
					
						|  TimQu | 36f27e4391 | Added a simple example model for multi-objective lra. | 5 years ago | 
				
					
						|  TimQu | 139c86f6a0 | Fixes for multi-obj LRA | 5 years ago | 
				
					
						|  TimQu | 400b69663a | Fixed multi-obj. tests | 5 years ago | 
				
					
						|  Tim Quatmann | e0276cb78f | Assertion fixed. | 5 years ago | 
				
					
						|  Tim Quatmann | d351bd6455 | WeightVectorChecker: Integrated lra objectives also in the individual phase | 5 years ago | 
				
					
						|  Tim Quatmann | 360c3877b7 | More steps towards integrating LRA in pcaa | 5 years ago | 
				
					
						|  Tim Quatmann | 43db81c18f | Silenced a warning. | 5 years ago | 
				
					
						|  Tim Quatmann | 67393a9584 | Further steps towards integrating LRA in weight vector checker. | 5 years ago | 
				
					
						|  Tim Quatmann | b3fa8893a2 | End Component Eliminator now also returns the sinkRows | 5 years ago | 
				
					
						|  Tim Quatmann | 29a7a7e865 | WeightVectorChecker: Making initialization LRA-ready | 5 years ago | 
				
					
						|  Tim Quatmann | 9421a60d5a | Fixes for multi-obj reward analysis. | 5 years ago | 
				
					
						|  Tim Quatmann | 4b13ad3220 | Fix for multi-obj LRA preprocessing | 5 years ago | 
				
					
						|  Tim Quatmann | 56e253fac0 | graph: Extended the documentation a tiny bit | 5 years ago | 
				
					
						|  Tim Quatmann | 33e73ed63a | WeightVectorChecker: Fixed incorrectly choosing a scheduler that potentially yields infinite reward for one objective. | 5 years ago | 
				
					
						|  Tim Quatmann | 4bf9bd473f | SparserMatrix: Added getRowGroupFilter method. | 5 years ago | 
				
					
						|  Sebastian Junges | 9df410e433 | Merge branch 'master' into monitoring | 5 years ago | 
				
					
						|  Sebastian Junges | b6be0f3356 | convex reduction | 5 years ago | 
				
					
						|  Sebastian Junges | d2e36e9db3 | dense belief states | 5 years ago | 
				
					
						|  Sebastian Junges | a358af1264 | set entries that are nonzero | 5 years ago | 
				
					
						|  Matthias Volk | f744176481 | Fixed lib filename for carl (Fixes #85) | 5 years ago | 
				
					
						|  Tim Quatmann | 7891492b96 | Merge branch 'master' into multi-objective-lra | 5 years ago | 
				
					
						|  Tim Quatmann | 94311e7d30 | Topological solvers: Added a warning for numerical issues triggered in cases where in non-exact mode a selfloop probability is very close to 1 but not equal to 1 | 5 years ago | 
				
					
						|  Tim Quatmann | 8a77e3238d | Implemented isAlmostZero and isAlmostOne also for non-double value types. | 5 years ago | 
				
					
						|  Tim Quatmann | d2f983a0c6 | Merge branch 'master' into multi-objective-lra | 5 years ago | 
				
					
						|  Tim Quatmann | 87456d00fc | Fixes in EdgeContainer::operator= | 5 years ago | 
				
					
						|  Tim Quatmann | ed1a5b6ced | Fixed flagging objectives for reward finiteness check incorrectly | 5 years ago | 
				
					
						|  Tim Quatmann | f79814bcb4 | Merge remote-tracking branch 'refs/remotes/origin/master' into multi-objective-lra | 5 years ago | 
				
					
						|  Tim Quatmann | 33a6687721 | Fixed deprecated operator= warnings | 5 years ago | 
				
					
						|  TimQu | 0e544a4c13 | Enabled TimeOperatorFormulas for multi-objective model checking of MDPs. | 5 years ago | 
				
					
						|  TimQu | 3db0ff124f | Started to make multiobjective reward analysis aware of LRA formulas. | 5 years ago | 
				
					
						|  TimQu | e898391e44 | Implemented stripping away of reward accumulations in multi-objective preprocessing. | 5 years ago | 
				
					
						|  TimQu | f532f6461b | The sparse StandardRewardModel somehow had 'dtmc' in it. | 5 years ago | 
				
					
						|  TimQu | 49bc9054b7 | Further improvements for filtered reward model | 5 years ago | 
				
					
						|  TimQu | 30977ed356 | Added some utility methods to reward path formulas | 5 years ago | 
				
					
						|  Matthias Volk | 825454d482 | Fixed warning | 5 years ago | 
				
					
						|  TimQu | 781fa9dbd8 | StandardRewardModel: Removed a default argument because the "default" constructor is ambiguous otherwise. | 5 years ago | 
				
					
						|  TimQu | f328e69dc4 | Added extract function to FilteredRewardModel | 5 years ago | 
				
					
						|  Matthias Volk | 55999036d6 | Fixed warning | 5 years ago | 
				
					
						|  TimQu | a5342d8b83 | added functionalities in MultiObjectivePreprocessorResult to capture lra objectives | 5 years ago | 
				
					
						|  TimQu | 74c1972c4a | Merge branch 'master' into multi-objective-lra | 5 years ago | 
				
					
						|  TimQu | 182f612272 | Enabled TimeOperatorFormulas for multi-objective model checking of MDPs. | 5 years ago | 
				
					
						|  TimQu | fa0ad07f8d | Added preprocessing of multi-objective lra formulas | 5 years ago | 
				
					
						|  TimQu | a5eb8e224b | Allowing lra formulas in multi-objective formula fragment | 5 years ago | 
				
					
						|  TimQu | 6902a3c8f8 | Revert "Fixed dot output of BDDs in sylvan." This reverts commit 6dcfd28186. | 5 years ago |