Translate.tla counterexample using modelator tla tla-trace-to-json-trace <filename> results in parsing error.

[danwt]

Bug:

Running ./modelator tla tla-trace-to-json-trace examples/counterexample1.tla does not work. Results in parsing error.

Content of counterexample.tla is at the bottom of this issue.

Expected:

JSON output for translated tla.

Log:

{
  "status": "error",
  "result": {
    "Nom": "Parsing Failure: Error { input: \"(((0\\n                  :> [creator |-> \\\"vt2\\\",\\n                    promiseId |-> 0,\\n                    type |-> \\\"vat\\\",\\n                    watchers |-> {}]\\n                @@ 1\\n                  :> [creator |-> \\\"None\\\",\\n                    promiseId |-> 0,\\n                    type |-> \\\"blank\\\",\\n                    watchers |-> {}])\\n              @@ 2\\n                :> [creator |-> \\\"None\\\",\\n                  promiseId |-> 0,\\n                  type |-> \\\"blank\\\",\\n                  watchers |-> {}])\\n            @@ 3\\n              :> [creator |-> \\\"vt1\\\",\\n                promiseId |-> 0,\\n                type |-> \\\"vat\\\",\\n                watchers |-> { \\\"vt0\\\", \\\"vt1\\\" }])\\n          @@ 4\\n            :> [creator |-> \\\"None\\\",\\n              promiseId |-> 0,\\n              type |-> \\\"blank\\\",\\n              watchers |-> {}])\\n        @@ 5\\n          :> [creator |-> \\\"None\\\",\\n            promiseId |-> 0,\\n            type |-> \\\"blank\\\",\\n            watchers |-> {}]\\n    /\\\\ cnt_promise = 0\\n    /\\\\ curr = \\\"vt0\\\"\\n    /\\\\ step = \\\"init\\\"\\n\\n(* Transition 3 to State1 *)\\n\", code: Satisfy }"
  }
}

Additional info:

Tested on release in (06ed539eb) latest

.tla file in question:

---------------------------- MODULE counterexample ----------------------------

EXTENDS MC_userspace

(* Constant initialization state *)
ConstInit == TRUE

(* Initial state *)
State0 ==
  bank
      = ((((0
                  :> [creator |-> "vt2",
                    promiseId |-> 0,
                    type |-> "vat",
                    watchers |-> {}]
                @@ 1
                  :> [creator |-> "None",
                    promiseId |-> 0,
                    type |-> "blank",
                    watchers |-> {}])
              @@ 2
                :> [creator |-> "None",
                  promiseId |-> 0,
                  type |-> "blank",
                  watchers |-> {}])
            @@ 3
              :> [creator |-> "vt1",
                promiseId |-> 0,
                type |-> "vat",
                watchers |-> { "vt0", "vt1" }])
          @@ 4
            :> [creator |-> "None",
              promiseId |-> 0,
              type |-> "blank",
              watchers |-> {}])
        @@ 5
          :> [creator |-> "None",
            promiseId |-> 0,
            type |-> "blank",
            watchers |-> {}]
    /\ cnt_promise = 0
    /\ curr = "vt0"
    /\ step = "init"

(* Transition 3 to State1 *)
State1 ==
  bank
      = ((((0
                  :> [creator |-> "vt2",
                    promiseId |-> 0,
                    type |-> "vat",
                    watchers |-> {}]
                @@ 3
                  :> [creator |-> "vt1",
                    promiseId |-> 0,
                    type |-> "vat",
                    watchers |-> { "vt0", "vt1" }])
              @@ 5
                :> [creator |-> "vt0",
                  promiseId |-> 1,
                  type |-> "promise",
                  watchers |-> {"vt0"}])
            @@ 1
              :> [creator |-> "vt0",
                promiseId |-> 1,
                type |-> "resolver",
                watchers |-> {"vt0"}])
          @@ 2
            :> [creator |-> "None",
              promiseId |-> 0,
              type |-> "blank",
              watchers |-> {}])
        @@ 4
          :> [creator |-> "None",
            promiseId |-> 0,
            type |-> "blank",
            watchers |-> {}]
    /\ cnt_promise = 1
    /\ curr = "vt0"
    /\ step = "storePromise"

(* Transition 1 to State2 *)
State2 ==
  bank
      = ((((3
                  :> [creator |-> "vt1",
                    promiseId |-> 0,
                    type |-> "vat",
                    watchers |-> { "vt0", "vt1" }]
                @@ 2
                  :> [creator |-> "None",
                    promiseId |-> 0,
                    type |-> "blank",
                    watchers |-> {}])
              @@ 0
                :> [creator |-> "vt2",
                  promiseId |-> 0,
                  type |-> "vat",
                  watchers |-> {}])
            @@ 1
              :> [creator |-> "vt0",
                promiseId |-> 1,
                type |-> "resolver",
                watchers |-> {"vt0"}])
          @@ 4
            :> [creator |-> "None",
              promiseId |-> 0,
              type |-> "blank",
              watchers |-> {}])
        @@ 5
          :> [creator |-> "vt0",
            promiseId |-> 1,
            type |-> "promise",
            watchers |-> {"vt0"}]
    /\ cnt_promise = 1
    /\ curr = "vt0"
    /\ step = "sendItem"

(* Transition 2 to State3 *)
State3 ==
  bank
      = ((((0
                  :> [creator |-> "vt2",
                    promiseId |-> 0,
                    type |-> "vat",
                    watchers |-> {}]
                @@ 2
                  :> [creator |-> "vt0",
                    promiseId |-> 0,
                    type |-> "vat",
                    watchers |-> {"vt0"}])
              @@ 1
                :> [creator |-> "vt0",
                  promiseId |-> 1,
                  type |-> "resolver",
                  watchers |-> {"vt0"}])
            @@ 3
              :> [creator |-> "vt1",
                promiseId |-> 0,
                type |-> "vat",
                watchers |-> { "vt0", "vt1" }])
          @@ 5
            :> [creator |-> "vt0",
              promiseId |-> 1,
              type |-> "promise",
              watchers |-> {"vt0"}])
        @@ 4
          :> [creator |-> "None",
            promiseId |-> 0,
            type |-> "blank",
            watchers |-> {}]
    /\ cnt_promise = 1
    /\ curr = "vt0"
    /\ step = "storeSelfRef"

(* Transition 4 to State4 *)
State4 ==
  bank
      = ((((0
                  :> [creator |-> "vt2",
                    promiseId |-> 0,
                    type |-> "vat",
                    watchers |-> {}]
                @@ 1
                  :> [creator |-> "None",
                    promiseId |-> 0,
                    type |-> "blank",
                    watchers |-> {}])
              @@ 3
                :> [creator |-> "vt1",
                  promiseId |-> 0,
                  type |-> "vat",
                  watchers |-> { "vt0", "vt1" }])
            @@ 4
              :> [creator |-> "None",
                promiseId |-> 0,
                type |-> "blank",
                watchers |-> {}])
          @@ 5
            :> [creator |-> "None",
              promiseId |-> 0,
              type |-> "blank",
              watchers |-> {}])
        @@ 2
          :> [creator |-> "vt0",
            promiseId |-> 0,
            type |-> "vat",
            watchers |-> {"vt0"}]
    /\ cnt_promise = 1
    /\ curr = "vt0"
    /\ step = "resolve"

(* Transition 0 to State5 *)
State5 ==
  bank
      = ((((3
                  :> [creator |-> "vt1",
                    promiseId |-> 0,
                    type |-> "vat",
                    watchers |-> { "vt0", "vt1" }]
                @@ 4
                  :> [creator |-> "None",
                    promiseId |-> 0,
                    type |-> "blank",
                    watchers |-> {}])
              @@ 5
                :> [creator |-> "None",
                  promiseId |-> 0,
                  type |-> "blank",
                  watchers |-> {}])
            @@ 0
              :> [creator |-> "vt2",
                promiseId |-> 0,
                type |-> "vat",
                watchers |-> {}])
          @@ 2
            :> [creator |-> "vt0",
              promiseId |-> 0,
              type |-> "vat",
              watchers |-> {"vt0"}])
        @@ 1
          :> [creator |-> "None",
            promiseId |-> 0,
            type |-> "blank",
            watchers |-> {}]
    /\ cnt_promise = 1
    /\ curr = "vt1"
    /\ step = "transferControl"

(* The following formula holds true in the last state and violates the invariant *)
InvariantViolation ==
  LET Call_hist ==
    <<
      [step |-> $C$6, curr |-> $C$152, cnt_promise |-> $C$8, bank |-> $C$68], [step |->
          $C$758,
        curr |-> $C$689,
        cnt_promise |-> $C$759,
        bank |-> $C$757], [step |-> $C$5430,
        curr |-> $C$5337,
        cnt_promise |-> $C$5431,
        bank |-> $C$5429], [step |-> $C$11472,
        curr |-> $C$11331,
        cnt_promise |-> $C$11473,
        bank |-> $C$11471], [step |-> $C$20258,
        curr |-> $C$20021,
        cnt_promise |-> $C$20259,
        bank |-> $C$20257], [step |-> $C$34539,
        curr |-> $C$34110,
        cnt_promise |-> $C$34540,
        bank |-> $C$34538]
    >>
  IN
  LET Example_si_2 ==
    { (Call_hist)[i$22]["step"]: i$22 \in DOMAIN Call_hist }
        = { "init",
          "resolve",
          "storePromise",
          "storeSelfRef",
          "unwatchSlot",
          "sendItem",
          "transferControl" }
      \/ { (Call_hist)[i$23]["step"]: i$23 \in DOMAIN Call_hist }
        = { "init",
          "resolve",
          "storePromise",
          "storeSelfRef",
          "sendItem",
          "transferControl" }
  IN
  Example_si_2

================================================================================
(* Created by Apalache on Fri Aug 13 09:44:40 BST 2021 *)
(* https://github.com/informalsystems/apalache *)

[rnbguy]

The current nom parser doesn't handle nested functions.

It will parse following successfully,

f = (p :> "-" @@ n :> "+")

but not this

f = (p :> "-" @@ (n :> "+"))

also not this

f = p :> "-" @@ n :> "+"

---

@danwt, it fails on the above counterexample.tla because bank variable is set with a nested function.

[rnbguy]

Sorry for the weekend work. I just had to finish the nested parser.

Anyway, this does not resolve the issue. Now it complains, it didn't parse the whole TlaState.

thread 'main' panicked at '[modelator] full TLA state should have been parsed', modelator/src/module/tla/json/mod.rs:10:13
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Looks like the states in TlaTrace are not correctly generated. Specifically impl FromStr for TlaTrace is buggy.

modelator/modelator/src/artifact/tla_trace.rs

Lines 26 to 30 in b45faeb

	impl FromStr for TlaTrace {
	type Err = Error;
	fn from_str(tla_trace: &str) -> Result<Self, Self::Err> {
	let lines = tla_trace.lines();

[rnbguy]

After a quick look, it seems,

• It doesn't handle comments.
• Relies on next State{} == keyword to stop adding more lines to stop for current state.
  • This allows the violated invariant to be added to the last state, causing Error.
  • Also adds the last ===== line from .tla files.

Removing those from .tla file does generate a proper trace.json.

[rnbguy]

@danwt I pushed a new TLA file parser. This should fix this issue :)

[rnbguy]

Looks like, the mentioned TLA file is not a proper TLA file. It should be the trace generated from modelator [tlc|apalache] test.

We have two choices.

1. rework the parser (very little work) to support both types of TLA files (proper syntax and trace)
2. generate the TLA trace with proper TLA syntax.

[rnbguy]

I went with option (2). TLA trace from modelator [checker] test will output a valid TLA file, which can be used for modelator tla tla-trace-to-json-trace.