prism-accumulation

3889 Commits

5 Branches

0 Tags

31 MiB

Tree: 1b1e41b384

Commit Graph

Author	SHA1	Message	Date
Dave Parker	17863ef170	Enable (explicit engine) model checking of LTSs. There is no explicit model type keyword added to the parser. Instead, LTSs are auto-detected by the absence of probabilities. ConstructModel is extended to build LTSs. Model checking (CTL+LTL) can be done out of the box using the existing NonProbModelChecker class. A few MDP regression tests are clarified to make it clear that the models are MDPs, not LTSs.	6 years ago
Dave Parker	99c06ba2d4	Move prism-tests into this repository and update Makefile "tests" target.	9 years ago

Author

SHA1

Message

Date

Dave Parker

17863ef170

Enable (explicit engine) model checking of LTSs.

There is no explicit model type keyword added to the parser.
Instead, LTSs are auto-detected by the absence of probabilities.

ConstructModel is extended to build LTSs. Model checking (CTL+LTL)
can be done out of the box using the existing NonProbModelChecker class.

A few MDP regression tests are clarified to make it clear that the
models are MDPs, not LTSs.

6 years ago

Dave Parker

99c06ba2d4

Move prism-tests into this repository and update Makefile "tests" target.

9 years ago

2 Commits (1b1e41b384581304a80ae136a6bbc29d3fb2b78f)