Tuesday, May 8, 2018

Behavioral Model Set

by Michał Antkiewicz, May 08, 2018

Clafer Model Wiki contains a few example models showcasing behavioral Clafer.
  1. TrafficLight. A simple state machine model for traffic light transitions.
  2. PowerWindow. Our main case study from the behavioral Clafer paper.
  3. WebSocketProtocol.
  4. TLS Handshake.

Thursday, February 1, 2018

Clafer Compiler 0.5.0 Released

by Michał Antkiewicz, Jan 31, 2018

This release contains only the Clafer compiler 0.5.0, which now includes support for modeling behavior. The release does not include reasoning capability; for structural modeling and reasoning keep using the previous release 0.4.5.

Binary builds are available from Clafer Tools - Binary Distributions.

Clafer compiler, release pull request (0.5.0).
  • support for behavioral modeling,
  • ability to compile, desugar, and render to HTML behavioral models,
  • test suite of behavioral models,
  • experimental Alloy code generator,
  • compatibility with GHC 8.2.2.
The Clafer model wiki is currently running Clafer 0.5.0.