[release] 0.9.0

[apalache-bot]

0.9.0

Features

• new sequential model checker that is using TransitionExecutor, see Sequential model checker using transition executor #467
• new command-line options, see Sequential model checker using transition executor #467 and the manual for details:
  • choose the algorithm: --algo=(offline|incremental)
  • pre-check, whether a transition disabled, discard the disabled transitions: --discard-disabled
  • do not check for deadlocks: --no-deadlock
  • pass tuning parameters in CLI: --tune-here
• parsing in-comment Java-like annotations, see [FEATURE] Parse annotations from the SANY comments #226
• tracking the source of variable/constant declarations and operator
  definitions in the TLA+ Parser, see [FEATURE] Extend operator declarations with annotations #262

Bug fixes

• the new sequential model checker has uncovered a bug that was not found
  by the old model checker, see Sequential model checker using transition executor #467

Documentation

• ADR004: In-comment annotations for declarations (of constants, variables, operators)