Skip to content

[FEATURE] Support PlusCal specs #1412

@lemmy

Description

@lemmy

The PlusCal translator removes all comments when translating an algorithm to TLA+.

---- MODULE Foo ----

(*--algorithm OneBitClock {
  variable
    \* @type: Int;
    clock \in {0, 1};
  {
    while (TRUE) {
      if (clock = 0)
        clock := 1
      else 
        clock := 0    
    }
  }
}*)
\* BEGIN TRANSLATION (chksum(pcal) = "d384ffcd" /\ chksum(tla) = "8dd09982")
VARIABLE clock

vars == << clock >>

Init == (* Global variables *)
        /\ clock \in {0, 1}

Next == IF clock = 0
           THEN /\ clock' = 1
           ELSE /\ clock' = 0

Spec == Init /\ [][Next]_vars

\* END TRANSLATION 
====

Metadata

Metadata

Assignees

Labels

newNew issue to be triaged.

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions