OPPAS v3.1.0

Changelog

• More user-friendly output format for POPACheck
• Add --stats flag to get old POPACheck output format
• Rename package to oppas
• Performance improvements to the probabilistic model checking engine
• Refactoring
• Bug fixes

OPPAS v3.0.0

Changelog

• Rename the suite to OPPAS
• Add POPACheck
• Support for probabilistic pushdown model checking
• Support for MiniProb inputs (MiniProc + probabilistic assignments and observations)

POMC v2.2.0

Changelog

• Add SMT-based model checking engine (only for finite-word model checking)
• MiniProc expressions can now be embedded in POTL formulas as atomic propositions
• Better logging infrastructure
• Bug fixes and performance improvements
• More tests and benchmarks

POMC v2.1.0

Changelog

• MiniProc now supports fixed-width integer variables and arrays
• MiniProc now supports non-deterministic variable assignments
• MiniProc functions now support local variables
• MiniProc functions now support passing arguments by value and value-result
• Better command-line arguments parsing
• Bugfixes and performance improvements
• More tests and benchmarks

POMC v2.0.0

New major release, now supporting infinite-word model checking.

Changelog:

• Support for infinite (or omega) word POTL model checking
• Better documentation
• Bug fixes and performance improvements

POMC v1.0.1

Minor release.

Changelog:

• MiniProc now supports module names
• Documentation improved

POMC v1.0.0

First stable release.

Changelog:

• Added MiniProc language for easily modelling procedural programs
• Output partial counterexample traces
• Added documentation sources
• Refactoring and performance optimizations

POMC v0.2.0

Changelog:

• Other files can now be included in .pomc input files
• Support for POTLv1 has been removed
• Several memory and performance optimizations

First release

First release with finite-word POTL model checking.