sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
1616 Commits
2 Branches
0 Tags
187 MiB
Tree: edfbfaa924
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'edfbfaa924'
${ noResults }
Commit Graph

205 Commits (edfbfaa924768d9e120685638a0e5f695a83976a)

Author SHA1 Message Date
masawei 4dca7abd3f Implementaed methods for checking until formula by providing the left and right states instead of the whole formula (same with bounded Until) in the SparseDtmcPrctlModelChecker, analouge to the SparseMdpPrctlModelChecker.
12 years ago
masawei 0cb390b186 More integration work.
12 years ago
masawei 4d161e5e8e Began with integration of crit. subsystem generation into master.
12 years ago
dehnert e3234b54f3 Step towards minimal command generator using MaxSAT and model checking.
12 years ago
dehnert a99bdf1b17 Switched to more elegant solution to query initial states of a model.
12 years ago
dehnert fdfb8ecc97 Minor fixes.
12 years ago
dehnert f39fb24f65 Removed pointers from Model Checker Interface (and callback methods in formulas). From now on, the results are returned in form of an object. Because of the existing move semantics for the types in question, this does not come at a performance penalty.
12 years ago
dehnert d8e85ec071 Removed guessing of initial scheduler as this was just an idea and not meant to be in master at this point.
12 years ago
PBerger e69c9f1962 Added all options from StoRM
12 years ago
dehnert 973e51bacb Beautified the code a bit.
12 years ago
dehnert b36b460a4e Added some comments to scheduler guessing.
12 years ago
dehnert d168b1848e Made GMRES and LSCG solution methods work for linear equation solving. Some further work on scheduler guessing.
12 years ago
dehnert 15542d46da Changes:
12 years ago
dehnert 36543de851 Started trying to implement a more clean iterator solution for sparse matrix.
12 years ago
dehnert 36f1306b4a Now schedulers get computed correctly.
12 years ago
dehnert 7e74bfbff2 Fixed bug in creation of scheduler, but there is still one really obvious one. Added small MDP example.
12 years ago
dehnert c3cc58d43b Revert to old starting point of value iteration. Tests run fine now.
12 years ago
dehnert 7095f8e67f Fixed a lot of issues introduced by refactoring.
12 years ago
dehnert abf6f85b63 Intermediate commit to switch workplace.
12 years ago
dehnert 69b0c4e236 On my way of implementing scheduler-guessing.
12 years ago
dehnert 7aa3139b62 Intermediate commit with submatrix computation for scheduler-induced system from MDP.
12 years ago
dehnert 04c7d5ba12 On my way of implementing scheduler-guessing.
12 years ago
PBerger cb770020bf Refactored the Jacobi Decomposition
12 years ago
dehnert f040264660 Intermediate commit with submatrix computation for scheduler-induced system from MDP.
12 years ago
dehnert f73342c56a Corrected color output in dot export of models. Fixed minimumOperator stack in SparseMdpPrctlModelChecker a bit, but this needs some further work.
12 years ago
PBerger 531293955a Added std::move() calls in SparseMdpPrctlModelChecker.h
12 years ago
PBerger b978a4d311 Added more move constructors.
12 years ago
dehnert e7601eb7b7 Included scheduler generation in model checking procedure for MDPs.
12 years ago
dehnert 16e1e2cedf Fixed wrong dimension bug in MDP model checkers.
12 years ago
Lanchid 81025757f8 Minor fix (Changed function name)
12 years ago
dehnert 65ebe3dcc3 Enabled check whether initial states are contained in the set of states for which the probability/reward values could be determined via graph algorithms to shorten computation times if possible.
12 years ago
dehnert f44f0ce410 Cleaned interfaces of models from std::shared_ptr. Improved some code in graph utility.
12 years ago
dehnert c8081c4d34 Fixed wrong step-bounded backward search.
12 years ago
dehnert 14fae4883a Added prob 0/1 precomputation for bounded-until model checking for DTMCs. The version for MDPs seems to perform worse: needs to be investigated.
12 years ago
dehnert a619303a1a Removed unnecessary command line utilities.
12 years ago
dehnert 64b883f695 Some cleanup in storm.cpp. Refactored and commented the utility module for vector operations.
12 years ago
Lanchid ec91dcbe2e Merge branch master into LTLParser
12 years ago
dehnert 92fe051924 Added some newlines.
12 years ago
dehnert 307911ca13 Fixed performance tests, they now run fine.
12 years ago
dehnert 3c32eec8e1 Made the prob0/1 algorithms for MDPs share a common backward transition object.
12 years ago
dehnert fbe1f41213 Removed GraphTransition class, which is now replaced by SparseMatrix in the instances where it was used before. Changed GraphAnalyzer accordingly and adapted tests.
12 years ago
Lanchid f9ab6f85d0 - Restructuration of model checkers (by logic)
12 years ago
dehnert 6ba1cf25c8 Added new variable for base bath for project root. Changed test input files to the files from example folder. Added leader4.lab to asynchronous leader election example.
12 years ago
dehnert 3851377064 Introduced executable storm-functional-tests and storm-performance-tests. While the former contains the previous tests, the latter is currently empty, but will hold performance tests in the future.
12 years ago
dehnert ab11d3c207 Further refactoring of GraphAnalyzer class. Some comments are still missing and GraphAnalyzer should be made a namespace instead of a class with static methods only.
12 years ago
dehnert fc67cf4e3f Further refactoring of GraphAnalyzer class.
12 years ago
dehnert cc7230abb1 Started to refactor graph analyzing to include less pointers and the like. Currently this breaks two tests.
12 years ago
Lanchid 065ac8f659 Basic command line interface for SToRM
12 years ago
dehnert f899914799 Adapted the labeling class such that no raw arrays are included any more, but a vector instead.
12 years ago
Lanchid cc242974dc Renamed namespace storm::formula to storm::property
12 years ago