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

83 Commits (d3124f2c235b66a79311e123d497b207f892b22d)

Author SHA1 Message Date
PBerger f63e5fc873 Implemented Policy Iteration inside the GmmxxMinMaxLinearEquationSolver.
10 years ago
dehnert be66ef2751 Finalized hybrid CTMC model checker.
10 years ago
dehnert 06bfc17ec6 Started making hybrid (dd/sparse) model checking work.
10 years ago
dehnert d787b80fec CTMC examples now build properly using the DD-based model generator.
10 years ago
dehnert 8f4a4397e0 Started working on Markovian commands in PRISM programs.
10 years ago
dehnert 1990567b84 Started to improve performance of sparse CTMC model checker.
10 years ago
dehnert 7fa6b568b4 Currently debugging the computation of transient probabilities in CTMCs.
10 years ago
David_Korzeniewski b623384dda Fixed merge errors and adapted to changes in master
10 years ago
dehnert 706ea56963 Now DDs are either MTBDDs or BDDs. This makes it possible to use BDDs where possible, which is faster.
10 years ago
dehnert f0b591be77 Further work on reintegrating parametric model checking into main executable.
10 years ago
dehnert 5794bbea56 Made some adaptions to make parametric model checking work in the main executable.
10 years ago
dehnert 534c8c8a44 Set more sensible default value for elimination order.
10 years ago
dehnert 197c242bb1 Some minor changes.
10 years ago
dehnert 1fb8d72a30 Merged master in parametricSystems.
10 years ago
dehnert 8a4706d9c9 A lot of work on model checker interfaces. In particular, the SCC elimination model checker is almost integrated.
10 years ago
dehnert b60c5ffdc0 Fixed a lot of tests, improved some things here and there.
10 years ago
David_Korzeniewski 78d3a392a5 Created settings module for TopologicalValueIterationNondeterministicLinearEquationSolver and integrated that with the solver.
10 years ago
svkurowski 67bcd5038f Add general setting to enable CUDA on runtime
10 years ago
dehnert 370a0ae476 Fixed some issues in bisimulation and added some tests.
10 years ago
dehnert 2f20abf47f The user can now select on the command line which reward model of a symbolic model is to be used (as a second [optional] argument to --symbolic).
10 years ago
svkurowski a4a15dd774 Add general setting to enable CUDA on runtime
10 years ago
dehnert 77d7555268 Added random order for state elimination.
10 years ago
dehnert 23c7c9b7d4 Further work on ordering options.
10 years ago
dehnert aa4836e085 Minor bugfix in bisimulation options.
10 years ago
dehnert a987233507 Started working on more options for sorting and integrating pure state elimination
10 years ago
dehnert 7257bb23c3 Further work on weak bisimulation. Model checking can now be done from tne command line again.
10 years ago
dehnert 391f3225e4 Added unparameterized NAND example. Further work on weak bisimulation.
10 years ago
dehnert 56aec18a48 Added bisimulation settings. Further work on weak bisimulation.
10 years ago
dehnert ca9dddb110 Sparse Bisimulation is still ongoing work.
10 years ago
sjunges d78d88b84d added export of constraints and resultfile
10 years ago
sjunges cafcb3f238 version info extended and moved to cpp, added options flag (although unclear what exactly should be displayed then)
10 years ago
dehnert caa7335afa Started work on sparse bisimulation decomposition.
10 years ago
dehnert 5571e2111c Changed default maximal SCC size to 20. Removed some debug output.
10 years ago
dehnert 385f7b7465 Added option to sort trivial SCC in descending order wrt. to their distances from the initial state. Added some more timing recordings.
10 years ago
dehnert 0776d8a74b Added and fixed some example models. Added option for maximal size of SCC that gets eliminated using state elimination.
10 years ago
dehnert 4eea90646a Fixed attributes of some example files. Added option to eliminate entry states in the very end (added option module for model checking of parametric models). Added feature to specify the formulas to check on the command line.
10 years ago
dehnert 428518ee12 Added some error checking to configuration file parsing.
10 years ago
dehnert 0a0485c8f0 Added the functionality to specify and parse a configuration file to set command line options.
10 years ago
dehnert 1f1b60e6de Added macros that can be used for printing and warnings. Included Dennis' fix for model checking of Markov automata. Added check methods to the settings modules that check whether the specified options are non-contradictive.
10 years ago
dehnert 96086cb6d8 Fixed a bug in the option system and MILP-based cex generator. Now everything should work for the demo. :)
10 years ago
dehnert 7d05c3d988 Added short name for counterexample generation option.
10 years ago
dehnert e49814d391 Modified pctl/csl/ltl options to now take formulas instead of files. Prefixed the macros with STORM_. Moved these macros into a file in the utilities. Modified architecture of the exception classes slightly. Threw away all the contents of main(). This will now be build from scratch.
10 years ago
dehnert 433bae1156 Switched from an option to fix deadlocks to an option to not fix the deadlocks. Hence, deadlocks are now fixed by default unless otherwise requested.
10 years ago
dehnert 2ba6f3e233 Fixed small bug in option system. Added simplifaction function calls to SCC-based reachability model checker.
10 years ago
dehnert 5ecc96fa3a Fixed some more places in the code to use the new option system.
10 years ago
dehnert 685d9274eb Help option now takes an argument that is interpreted as a regexp and matched against the module names and option names.
10 years ago
dehnert 7e56e0d8f7 Added feature to also show help for a given option name.
10 years ago
dehnert a995d7dd4a The tests now run fine with the new option system.
10 years ago
dehnert 266d660d89 Added functions responsible for printing the help. Started adapting the tests to the new option system.
10 years ago
dehnert 46dc2ca05a Further work on option system (we're getting there...).
10 years ago