TLA+

DASL (DAU Automation Specification Language) is a formal specification language for industrial automation, which allows us to use TLA+/TLC to reason about the specification and to generate Go code implementing the formal specification. The formal DASL specification is embedded in code blocks inside markdown files allowing us to describe our formal specification in natural language in one document. DASL is made with gogll Background When developing complex systems we are always confronted by the problem of specifying the system to be built in such a way that we can reason about its behaviour without drowning in implementation detail. [Read More]