Changelog

All notable changes to this project will be documented in this file.

The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.

As a minor extension, we also keep a semantic version for the UNRELEASED changes.

UNRELEASED

3.0.0 - 2023-02-14

• BREAKING: Add HasVariables class to keep track of symbolic variables and automatically insert precondition checks for well-scopedness of variables.
• BREAKING: Remove some unnecessary and unusead features in dynamic logic, including re-running tests from a counterexample directly.
• Improved printing of counterexamples in DL - they are now printed as code that can be copied more-or-less verbatim to create a runnable counterexample in code.
• Made the variable context explicit to avoid having to keep track of symbolic variables in the model
  • This introduces the ctxAtType and arbitraryVar functions to use in action generators (c.f. the RegistryModel.hs example).

2.0.0 - 2022-10-11

• BREAKING: Add Realized type family to distinguish between the model- and real type of an action
• BREAKING: Introduce RunModel type class to interpret Model-generated sequence of actions against real-world implementation
  • Move perform method from StateModel to this new type-class
  • Also split postcondition and monitoring out from the StateModel to the RunModel type class
• Added Thread registry example based on io-sim concurrency simulation library

1.1.0 - 2022-08-27

• Fix broken links in Hackage-generated documentation and link to other Quviq papers
• Add Show a constraint on monitoring

1.0.0

• Initial publication of quickcheck-dynamic library on Hackage
• Provide base StateModel and DynamicLogic tools to write quickcheck-based models, express properties, and test them