learning:faq

This is an old revision of the document!


PHP's gd library is missing or unable to create PNG images

FAQ

No, state trace for violated temporal properties is not supported.

TLA+ specifications are built using:

  • Actions: These represent atomic state transitions in the system.
  • State predicates: Boolean expressions that describe properties of a single state.
  • Temporal operators: These connect actions and state predicates to describe how the system's behavior evolves over time.
  • learning/faq.1729297628.txt.gz
  • Last modified: 2024/10/19 00:27
  • by fponzi