v0.2.8

Changelog

new features 🎉

• enhance token positioning in interactive counter example exploration pages

v0.2.7

Changelog

new features 🎉

• generate interactive counter example exploration pages

v0.2.6

Changelog

new features 🎉

• generate pictures for counter examples (via dot)

v0.2.5

Changelog

new features 🎉

• subset of BPMN
  • support message boundary events on all activities (tasks and subprocesses)
• verification script (for Linux and OSX)
  • check requisites
  • add option to chose the number of workers (process cores used in verification)

bugfix 🐛

• TLA+ theories for the BPMN execution semantics
  • move message reception in receive tasks after activation
  • add well-formedness condition for subprocesses to begin with a none start event
  • correct subprocess completion in case of multiple end events

v0.2.4

Changelog

new features 🎉

• TLA+ theories for the BPMN execution semantics
  • add parameter to enable re-entrance or not for activities
• verification script (for Linux and OSX)
  • enhanced ouput

v0.2.3

Changelog

bugfix 🐛

• TLA+ theories for the BPMN execution semantics
  • boundary event interruption also removes tokens on edges
  • boundary event interruption cannot happen upon sub process termination

v0.2.2

Changelog

new features 🎉

• TLA+ theories for the BPMN execution semantics
  • support bounding constraints to deal with unbounded models

breaking changes ⚠️

• TLA+ theories for the BPMN execution semantics
  • use new syntax for boundary events
  • update some type names to better suit the BPMN meta-model

v0.2.1

Changelog

new features 🎉

• verification script (for Linux and OSX)
  • perform automatically the verification for the different communication modes x different properties

v0.2.0

Changelog

new features 🎉

• subset of BPMN
  • support message boundary events (interrupting or not) for sub processes

v0.1.1

Changelog

bugfix 🐛

• verification script (for Linux and OSX)
  • correct error message for TLA2TOOLS_HOME