Introduce an exporter of TlaEx and TlaModule to JSON

[konnov]

This will allow us to export counterexamples and the intermediate representation in a machine-readable format that does not require other tools to parse TLA+.

[lemmy]

FYI: I considered to add similar functionality to TLC, but eventually decided not to and instead start a JSON module that has operators to convert TLA+ expressions into JSON.

By the way, it seems somebody from the community is going to extend the module.

[konnov]

That is fun! You can only to in TLC though :-)

Our main motivation for doing that is to export counterexamples in a way that would easy integration with other tools. We should think about maintaining compatibility with your translation then.

[lemmy]

Exporting traces was the main motivation for the JSON module too. JSON may be en-vogue today but the trend will undoubtedly swing back to schema-based formats eventually.

Anyway, since both TLC and Apalache are (essentially) Java, can't Apalache simply invoke TLC internally to convert a counterexample to JSON? By the way, I wondered about the same thing when I saw Apalache's TLC config parser: Why not call TLC's code from Apalache?! We can probably expose TLC's classes if that's the problem.

[konnov]

Well, to call TLC, we would have to reconstruct the expressions using SemanticNode. This is a tough exercise. Our IR is much simpler.

[lemmy]

Can't you go IR > TLA+ > SANY > ... In other words, go from your IR back to TLA+ and the through SANY.

Anyway, what I trying to say is that please let me know in case changes in TLC would simplify work in Apalache.

[konnov]

I have not thought about IR -> TLA+ -> SANY. That is a good stress test for the whole tool chain :-)

[andrey-kuprianov]

Hi Markus!

thank you for the ideas and suggestions regarding usage of TLC from Apalache!

I also want to point out the the other direction is possible, i.e. call Apalache from TLC if a JSON conversion is needed. I've just finished to implement it -- if interested, please checkout the branch "ak/jsonprinter" (or "unstable" next week -- then the PR will be merged already, hopefully)

-- Andrey

On Fri, Feb 7, 2020 at 4:41 PM Markus Alexander Kuppe < notifications@github.com> wrote:

Can't you go IR > TLA+ > SANY > ... In other words, go from your IR back to TLA+ and the through SANY.

Anyway, what I trying to say is that please let me know in case changes in TLC would simplify work in Apalache.

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/konnov/apalache/issues/77?email_source=notifications&email_token=AOF3ZPSFZEX53WNIOSJGW4TRBV6I7A5CNFSM4JXNTQK2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOELDOC6Y#issuecomment-583459195, or unsubscribe https://github.com/notifications/unsubscribe-auth/AOF3ZPWASBAN7YSPLCQKJHDRBV6I7ANCNFSM4JXNTQKQ .

[lemmy]

@andrey-kuprianov Please elaborate. Do you mean we can programmatically call Apalache from TLC or are you saying that we can feed a TLC error trace (or the equivalent TLA+ trace) to Apalache for conversion?

[andrey-kuprianov]

Currently, if you call apalache-mc parse <file.tla> the JSON encoding of it will be output to a subdirectory x/..../file.json. We can also easily add whatever option is considered helpful, if this is not enough.

About programmatic access -- this question should be addressed to Igor, I am not yet familiar enough with the codebase of either Apalache or TLC to answer it...

On Fri, Feb 7, 2020 at 5:04 PM Markus Alexander Kuppe < notifications@github.com> wrote:

@andrey-kuprianov https://github.com/andrey-kuprianov Please elaborate. Do you mean we can programmatically call Apalache from TLC or are you saying that we can feed a TLC error trace (or the equivalent TLA+ trace) to Apalache for conversion?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/konnov/apalache/issues/77?email_source=notifications&email_token=AOF3ZPX5DP22AVDTYZTK4FTRBWBCNA5CNFSM4JXNTQK2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOELDRELY#issuecomment-583471663, or unsubscribe https://github.com/notifications/unsubscribe-auth/AOF3ZPWPZTG54TRJO5IYF4DRBWBCNANCNFSM4JXNTQKQ .

[lemmy]

apalache-mc parse ... seems to work great:

I just checked BlockingQueue.tla with TLC's -generateSpecTE to create SpecTE.tla. apalache converted SpecTE.tla to the JSON below.

Follow-up questions: Does this work without z3 being present?

--------------------------- MODULE SpecTE ----
EXTENDS Sequences, Naturals, TLC, FiniteSets

\* 
\*  SpecTE follows
\* 

a <: b == a

CONSTANTS Producers,   (* the (nonempty) set of producers                       *)
          Consumers,   (* the (nonempty) set of consumers                       *)
          BufCapacity  (* the maximum number of messages in the bounded buffer  *)

ConstInit ==
  /\ Producers = {"p1","p2","p3","p4"}
  /\ Consumers = {"c1","c2","c3"}
  /\ BufCapacity = 3

ASSUME Assumption ==
       /\ Producers # {}                      (* at least one producer *)
       /\ Consumers # {}                      (* at least one consumer *)
       /\ Producers \intersect Consumers = {} (* no thread is both consumer and producer *)
       /\ BufCapacity \in (Nat \ {0})         (* buffer capacity is at least 1 *)

-----------------------------------------------------------------------------

VARIABLES buffer, waitSet
vars == <<buffer, waitSet>>

RunningThreads == (Producers \cup Consumers) \ waitSet

(* @see java.lang.Object#notify *)       
Notify == IF waitSet # ({} <: {STRING}) \* {}
          THEN \E x \in waitSet: waitSet' = waitSet \ {x}
          ELSE UNCHANGED waitSet

(* @see java.lang.Object#wait *)
Wait(t) == /\ waitSet' = waitSet \cup {t}
           /\ UNCHANGED <<buffer>>

-----------------------------------------------------------------------------

Put(t, d) ==
   \/ /\ Len(buffer) < BufCapacity
      /\ buffer' = Append(buffer, d)
      /\ Notify
   \/ /\ Len(buffer) = BufCapacity
      /\ Wait(t)

Get(t) ==
   \/ /\ buffer # <<>> <: Seq(STRING) \* <<>>
      /\ buffer' = Tail(buffer)
      /\ Notify
   \/ /\ buffer = <<>> <: Seq(STRING) \*
      /\ Wait(t)

-----------------------------------------------------------------------------

(* Initially, the buffer is empty and no thread is waiting. *)
Init == /\ buffer = (<<>> <: Seq(STRING))
        /\ waitSet = ({} <: {STRING})

(* Then, pick a thread out of all running threads and have it do its thing. *)
Next == \E t \in RunningThreads: \/ /\ t \in Producers
                                    /\ Put(t, t) \* Add some data to buffer
                                 \/ /\ t \in Consumers
                                    /\ Get(t)

Invariant == waitSet # (Producers \cup Consumers)

CONSTANTS c3, p1, p2, p3, p4, c1, c2

\* TRACE Sub-Action definition 0
Next_sa_0 ==
    (
        /\ buffer = (<<>>)
        /\ waitSet = ({})
        /\ buffer' = (<<p1>>)
        /\ waitSet' = ({})
    )

\* TRACE Sub-Action definition 1
Next_sa_1 ==
    (
        /\ buffer = (<<p1>>)
        /\ waitSet = ({})
        /\ buffer' = (<<p1, p1>>)
        /\ waitSet' = ({})
    )

\* TRACE Sub-Action definition 2
Next_sa_2 ==
    (
        /\ buffer = (<<p1, p1>>)
        /\ waitSet = ({})
        /\ buffer' = (<<p1, p1, p1>>)
        /\ waitSet' = ({})
    )

\* TRACE Sub-Action definition 3
Next_sa_3 ==
    (
        /\ buffer = (<<p1, p1, p1>>)
        /\ waitSet = ({})
        /\ buffer' = (<<p1, p1, p1>>)
        /\ waitSet' = ({p1})
    )

\* TRACE Sub-Action definition 4
Next_sa_4 ==
    (
        /\ buffer = (<<p1, p1, p1>>)
        /\ waitSet = ({p1})
        /\ buffer' = (<<p1, p1, p1>>)
        /\ waitSet' = ({p1, p2})
    )

\* TRACE Sub-Action definition 5
Next_sa_5 ==
    (
        /\ buffer = (<<p1, p1, p1>>)
        /\ waitSet = ({p1, p2})
        /\ buffer' = (<<p1, p1, p1>>)
        /\ waitSet' = ({p1, p2, p3})
    )

\* TRACE Sub-Action definition 6
Next_sa_6 ==
    (
        /\ buffer = (<<p1, p1, p1>>)
        /\ waitSet = ({p1, p2, p3})
        /\ buffer' = (<<p1, p1, p1>>)
        /\ waitSet' = ({p1, p2, p3, p4})
    )

\* TRACE Sub-Action definition 7
Next_sa_7 ==
    (
        /\ buffer = (<<p1, p1, p1>>)
        /\ waitSet = ({p1, p2, p3, p4})
        /\ buffer' = (<<p1, p1>>)
        /\ waitSet' = ({p2, p3, p4})
    )

\* TRACE Sub-Action definition 8
Next_sa_8 ==
    (
        /\ buffer = (<<p1, p1>>)
        /\ waitSet = ({p2, p3, p4})
        /\ buffer' = (<<p1>>)
        /\ waitSet' = ({p3, p4})
    )

\* TRACE Sub-Action definition 9
Next_sa_9 ==
    (
        /\ buffer = (<<p1>>)
        /\ waitSet = ({p3, p4})
        /\ buffer' = (<<>>)
        /\ waitSet' = ({p4})
    )

\* TRACE Sub-Action definition 10
Next_sa_10 ==
    (
        /\ buffer = (<<>>)
        /\ waitSet = ({p4})
        /\ buffer' = (<<>>)
        /\ waitSet' = ({p4, c1})
    )

\* TRACE Sub-Action definition 11
Next_sa_11 ==
    (
        /\ buffer = (<<>>)
        /\ waitSet = ({p4, c1})
        /\ buffer' = (<<>>)
        /\ waitSet' = ({p4, c1, c2})
    )

\* TRACE Sub-Action definition 12
Next_sa_12 ==
    (
        /\ buffer = (<<>>)
        /\ waitSet = ({p4, c1, c2})
        /\ buffer' = (<<>>)
        /\ waitSet' = ({p4, c1, c2, c3})
    )

\* TRACE Sub-Action definition 13
Next_sa_13 ==
    (
        /\ buffer = (<<>>)
        /\ waitSet = ({p4, c1, c2, c3})
        /\ buffer' = (<<p1>>)
        /\ waitSet' = ({c1, c2, c3})
    )

\* TRACE Sub-Action definition 14
Next_sa_14 ==
    (
        /\ buffer = (<<p1>>)
        /\ waitSet = ({c1, c2, c3})
        /\ buffer' = (<<p1, p1>>)
        /\ waitSet' = ({c2, c3})
    )

\* TRACE Sub-Action definition 15
Next_sa_15 ==
    (
        /\ buffer = (<<p1, p1>>)
        /\ waitSet = ({c2, c3})
        /\ buffer' = (<<p1, p1, p1>>)
        /\ waitSet' = ({c3})
    )

\* TRACE Sub-Action definition 16
Next_sa_16 ==
    (
        /\ buffer = (<<p1, p1, p1>>)
        /\ waitSet = ({c3})
        /\ buffer' = (<<p1, p1, p1>>)
        /\ waitSet' = ({p1, c3})
    )

\* TRACE Sub-Action definition 17
Next_sa_17 ==
    (
        /\ buffer = (<<p1, p1, p1>>)
        /\ waitSet = ({p1, c3})
        /\ buffer' = (<<p1, p1, p1>>)
        /\ waitSet' = ({p1, p2, c3})
    )

\* TRACE Sub-Action definition 18
Next_sa_18 ==
    (
        /\ buffer = (<<p1, p1, p1>>)
        /\ waitSet = ({p1, p2, c3})
        /\ buffer' = (<<p1, p1, p1>>)
        /\ waitSet' = ({p1, p2, p3, c3})
    )

\* TRACE Sub-Action definition 19
Next_sa_19 ==
    (
        /\ buffer = (<<p1, p1, p1>>)
        /\ waitSet = ({p1, p2, p3, c3})
        /\ buffer' = (<<p1, p1, p1>>)
        /\ waitSet' = ({p1, p2, p3, p4, c3})
    )

\* TRACE Sub-Action definition 20
Next_sa_20 ==
    (
        /\ buffer = (<<p1, p1, p1>>)
        /\ waitSet = ({p1, p2, p3, p4, c3})
        /\ buffer' = (<<p1, p1>>)
        /\ waitSet' = ({p2, p3, p4, c3})
    )

\* TRACE Sub-Action definition 21
Next_sa_21 ==
    (
        /\ buffer = (<<p1, p1>>)
        /\ waitSet = ({p2, p3, p4, c3})
        /\ buffer' = (<<p1>>)
        /\ waitSet' = ({p3, p4, c3})
    )

\* TRACE Sub-Action definition 22
Next_sa_22 ==
    (
        /\ buffer = (<<p1>>)
        /\ waitSet = ({p3, p4, c3})
        /\ buffer' = (<<>>)
        /\ waitSet' = ({p3, p4})
    )

\* TRACE Sub-Action definition 23
Next_sa_23 ==
    (
        /\ buffer = (<<>>)
        /\ waitSet = ({p3, p4})
        /\ buffer' = (<<>>)
        /\ waitSet' = ({p3, p4, c1})
    )

\* TRACE Sub-Action definition 24
Next_sa_24 ==
    (
        /\ buffer = (<<>>)
        /\ waitSet = ({p3, p4, c1})
        /\ buffer' = (<<>>)
        /\ waitSet' = ({p3, p4, c1, c2})
    )

\* TRACE Sub-Action definition 25
Next_sa_25 ==
    (
        /\ buffer = (<<>>)
        /\ waitSet = ({p3, p4, c1, c2})
        /\ buffer' = (<<>>)
        /\ waitSet' = ({p3, p4, c1, c2, c3})
    )

\* TRACE Sub-Action definition 26
Next_sa_26 ==
    (
        /\ buffer = (<<>>)
        /\ waitSet = ({p3, p4, c1, c2, c3})
        /\ buffer' = (<<p1>>)
        /\ waitSet' = ({p4, c1, c2, c3})
    )

\* TRACE Sub-Action definition 27
Next_sa_27 ==
    (
        /\ buffer = (<<p1>>)
        /\ waitSet = ({p4, c1, c2, c3})
        /\ buffer' = (<<p1, p1>>)
        /\ waitSet' = ({c1, c2, c3})
    )

\* TRACE Sub-Action definition 28
Next_sa_28 ==
    (
        /\ buffer = (<<p1, p1>>)
        /\ waitSet = ({c1, c2, c3})
        /\ buffer' = (<<p1, p1, p1>>)
        /\ waitSet' = ({c2, c3})
    )

\* TRACE Sub-Action definition 29
Next_sa_29 ==
    (
        /\ buffer = (<<p1, p1, p1>>)
        /\ waitSet = ({c2, c3})
        /\ buffer' = (<<p1, p1, p1>>)
        /\ waitSet' = ({p1, c2, c3})
    )

\* TRACE Sub-Action definition 30
Next_sa_30 ==
    (
        /\ buffer = (<<p1, p1, p1>>)
        /\ waitSet = ({p1, c2, c3})
        /\ buffer' = (<<p1, p1, p1>>)
        /\ waitSet' = ({p1, p2, c2, c3})
    )

\* TRACE Sub-Action definition 31
Next_sa_31 ==
    (
        /\ buffer = (<<p1, p1, p1>>)
        /\ waitSet = ({p1, p2, c2, c3})
        /\ buffer' = (<<p1, p1, p1>>)
        /\ waitSet' = ({p1, p2, p3, c2, c3})
    )

\* TRACE Sub-Action definition 32
Next_sa_32 ==
    (
        /\ buffer = (<<p1, p1, p1>>)
        /\ waitSet = ({p1, p2, p3, c2, c3})
        /\ buffer' = (<<p1, p1, p1>>)
        /\ waitSet' = ({p1, p2, p3, p4, c2, c3})
    )

\* TRACE Sub-Action definition 33
Next_sa_33 ==
    (
        /\ buffer = (<<p1, p1, p1>>)
        /\ waitSet = ({p1, p2, p3, p4, c2, c3})
        /\ buffer' = (<<p1, p1>>)
        /\ waitSet' = ({p2, p3, p4, c2, c3})
    )

\* TRACE Sub-Action definition 34
Next_sa_34 ==
    (
        /\ buffer = (<<p1, p1>>)
        /\ waitSet = ({p2, p3, p4, c2, c3})
        /\ buffer' = (<<p1>>)
        /\ waitSet' = ({p2, p3, p4, c3})
    )

\* TRACE Sub-Action definition 35
Next_sa_35 ==
    (
        /\ buffer = (<<p1>>)
        /\ waitSet = ({p2, p3, p4, c3})
        /\ buffer' = (<<>>)
        /\ waitSet' = ({p2, p3, p4})
    )

\* TRACE Sub-Action definition 36
Next_sa_36 ==
    (
        /\ buffer = (<<>>)
        /\ waitSet = ({p2, p3, p4})
        /\ buffer' = (<<>>)
        /\ waitSet' = ({p2, p3, p4, c1})
    )

\* TRACE Sub-Action definition 37
Next_sa_37 ==
    (
        /\ buffer = (<<>>)
        /\ waitSet = ({p2, p3, p4, c1})
        /\ buffer' = (<<>>)
        /\ waitSet' = ({p2, p3, p4, c1, c2})
    )

\* TRACE Sub-Action definition 38
Next_sa_38 ==
    (
        /\ buffer = (<<>>)
        /\ waitSet = ({p2, p3, p4, c1, c2})
        /\ buffer' = (<<>>)
        /\ waitSet' = ({p2, p3, p4, c1, c2, c3})
    )

\* TRACE Sub-Action definition 39
Next_sa_39 ==
    (
        /\ buffer = (<<>>)
        /\ waitSet = ({p2, p3, p4, c1, c2, c3})
        /\ buffer' = (<<p1>>)
        /\ waitSet' = ({p3, p4, c1, c2, c3})
    )

\* TRACE Sub-Action definition 40
Next_sa_40 ==
    (
        /\ buffer = (<<p1>>)
        /\ waitSet = ({p3, p4, c1, c2, c3})
        /\ buffer' = (<<p1, p1>>)
        /\ waitSet' = ({p4, c1, c2, c3})
    )

\* TRACE Sub-Action definition 41
Next_sa_41 ==
    (
        /\ buffer = (<<p1, p1>>)
        /\ waitSet = ({p4, c1, c2, c3})
        /\ buffer' = (<<p1, p1, p1>>)
        /\ waitSet' = ({c1, c2, c3})
    )

\* TRACE Sub-Action definition 42
Next_sa_42 ==
    (
        /\ buffer = (<<p1, p1, p1>>)
        /\ waitSet = ({c1, c2, c3})
        /\ buffer' = (<<p1, p1, p1>>)
        /\ waitSet' = ({p1, c1, c2, c3})
    )

\* TRACE Sub-Action definition 43
Next_sa_43 ==
    (
        /\ buffer = (<<p1, p1, p1>>)
        /\ waitSet = ({p1, c1, c2, c3})
        /\ buffer' = (<<p1, p1, p1>>)
        /\ waitSet' = ({p1, p2, c1, c2, c3})
    )

\* TRACE Sub-Action definition 44
Next_sa_44 ==
    (
        /\ buffer = (<<p1, p1, p1>>)
        /\ waitSet = ({p1, p2, c1, c2, c3})
        /\ buffer' = (<<p1, p1, p1>>)
        /\ waitSet' = ({p1, p2, p3, c1, c2, c3})
    )

\* TRACE Action Constraint definition traceExploreActionConstraint
_SpecTEActionConstraint ==
<<
Next_sa_0,
Next_sa_1,
Next_sa_2,
Next_sa_3,
Next_sa_4,
Next_sa_5,
Next_sa_6,
Next_sa_7,
Next_sa_8,
Next_sa_9,
Next_sa_10,
Next_sa_11,
Next_sa_12,
Next_sa_13,
Next_sa_14,
Next_sa_15,
Next_sa_16,
Next_sa_17,
Next_sa_18,
Next_sa_19,
Next_sa_20,
Next_sa_21,
Next_sa_22,
Next_sa_23,
Next_sa_24,
Next_sa_25,
Next_sa_26,
Next_sa_27,
Next_sa_28,
Next_sa_29,
Next_sa_30,
Next_sa_31,
Next_sa_32,
Next_sa_33,
Next_sa_34,
Next_sa_35,
Next_sa_36,
Next_sa_37,
Next_sa_38,
Next_sa_39,
Next_sa_40,
Next_sa_41,
Next_sa_42,
Next_sa_43,
Next_sa_44
>>[TLCGet("level")]
----

def_ov_15810930190442000 == 
<<
([buffer |-> <<>>,waitSet |-> {}]),
([buffer |-> <<p1>>,waitSet |-> {}]),
([buffer |-> <<p1, p1>>,waitSet |-> {}]),
([buffer |-> <<p1, p1, p1>>,waitSet |-> {}]),
([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1}]),
([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2}]),
([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2, p3}]),
([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2, p3, p4}]),
([buffer |-> <<p1, p1>>,waitSet |-> {p2, p3, p4}]),
([buffer |-> <<p1>>,waitSet |-> {p3, p4}]),
([buffer |-> <<>>,waitSet |-> {p4}]),
([buffer |-> <<>>,waitSet |-> {p4, c1}]),
([buffer |-> <<>>,waitSet |-> {p4, c1, c2}]),
([buffer |-> <<>>,waitSet |-> {p4, c1, c2, c3}]),
([buffer |-> <<p1>>,waitSet |-> {c1, c2, c3}]),
([buffer |-> <<p1, p1>>,waitSet |-> {c2, c3}]),
([buffer |-> <<p1, p1, p1>>,waitSet |-> {c3}]),
([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, c3}]),
([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2, c3}]),
([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2, p3, c3}]),
([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2, p3, p4, c3}]),
([buffer |-> <<p1, p1>>,waitSet |-> {p2, p3, p4, c3}]),
([buffer |-> <<p1>>,waitSet |-> {p3, p4, c3}]),
([buffer |-> <<>>,waitSet |-> {p3, p4}]),
([buffer |-> <<>>,waitSet |-> {p3, p4, c1}]),
([buffer |-> <<>>,waitSet |-> {p3, p4, c1, c2}]),
([buffer |-> <<>>,waitSet |-> {p3, p4, c1, c2, c3}]),
([buffer |-> <<p1>>,waitSet |-> {p4, c1, c2, c3}]),
([buffer |-> <<p1, p1>>,waitSet |-> {c1, c2, c3}]),
([buffer |-> <<p1, p1, p1>>,waitSet |-> {c2, c3}]),
([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, c2, c3}]),
([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2, c2, c3}]),
([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2, p3, c2, c3}]),
([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2, p3, p4, c2, c3}]),
([buffer |-> <<p1, p1>>,waitSet |-> {p2, p3, p4, c2, c3}]),
([buffer |-> <<p1>>,waitSet |-> {p2, p3, p4, c3}]),
([buffer |-> <<>>,waitSet |-> {p2, p3, p4}]),
([buffer |-> <<>>,waitSet |-> {p2, p3, p4, c1}]),
([buffer |-> <<>>,waitSet |-> {p2, p3, p4, c1, c2}]),
([buffer |-> <<>>,waitSet |-> {p2, p3, p4, c1, c2, c3}]),
([buffer |-> <<p1>>,waitSet |-> {p3, p4, c1, c2, c3}]),
([buffer |-> <<p1, p1>>,waitSet |-> {p4, c1, c2, c3}]),
([buffer |-> <<p1, p1, p1>>,waitSet |-> {c1, c2, c3}]),
([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, c1, c2, c3}]),
([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2, c1, c2, c3}]),
([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2, p3, c1, c2, c3}])
>>
----

\* VARIABLE TraceExp

\* TRACE INIT definition traceExploreInit
_SpecTEInit ==
    /\ buffer = (
            <<>>
        )
    /\ waitSet = (
            {}
        )
\*     /\ TraceExp = TRUE

----

\* TRACE NEXT definition traceExploreNext
_SpecTENext ==
/\  \/ Next_sa_0
    \/ Next_sa_1
    \/ Next_sa_2
    \/ Next_sa_3
    \/ Next_sa_4
    \/ Next_sa_5
    \/ Next_sa_6
    \/ Next_sa_7
    \/ Next_sa_8
    \/ Next_sa_9
    \/ Next_sa_10
    \/ Next_sa_11
    \/ Next_sa_12
    \/ Next_sa_13
    \/ Next_sa_14
    \/ Next_sa_15
    \/ Next_sa_16
    \/ Next_sa_17
    \/ Next_sa_18
    \/ Next_sa_19
    \/ Next_sa_20
    \/ Next_sa_21
    \/ Next_sa_22
    \/ Next_sa_23
    \/ Next_sa_24
    \/ Next_sa_25
    \/ Next_sa_26
    \/ Next_sa_27
    \/ Next_sa_28
    \/ Next_sa_29
    \/ Next_sa_30
    \/ Next_sa_31
    \/ Next_sa_32
    \/ Next_sa_33
    \/ Next_sa_34
    \/ Next_sa_35
    \/ Next_sa_36
    \/ Next_sa_37
    \/ Next_sa_38
    \/ Next_sa_39
    \/ Next_sa_40
    \/ Next_sa_41
    \/ Next_sa_42
    \/ Next_sa_43
    \/ Next_sa_44
\* /\ TraceExp' = TraceExp

=============================================================================

out-parser-json.txt

[andrey-kuprianov]

glad to hear it worked well for you:) I have some ideas on improving the encoding, will let you know tomorrow when this is done.

as for your question: to the best of my knowledge -- no; from my experience it won't compile without Z3... but it's probably a good idea to make Apalache lazy wrt. to the modules it uses.

On Fri, Feb 7, 2020 at 9:20 PM Markus Alexander Kuppe < notifications@github.com> wrote:

apalache-mc parse ... seems to work great:

I just checked BlockingQueue.tla https://github.com/lemmy/BlockingQueue/blob/50c1ad56062c32d862b8d3d3b06ae17c05f466e8/BlockingQueue.tla with TLC's -generateSpecTE to create SpecTE.tla. apalache converted SpecTE.tla to the JSON below.

Follow-up questions: Does this work without z3 being present?

--------------------------- MODULE SpecTE ----EXTENDS Sequences, Naturals, TLC, FiniteSets * * SpecTE follows*

a <: b == a CONSTANTS Producers, ( the (nonempty) set of producers ) Consumers, ( the (nonempty) set of consumers ) BufCapacity ( the maximum number of messages in the bounded buffer )

ConstInit == /\ Producers = {"p1","p2","p3","p4"} /\ Consumers = {"c1","c2","c3"} /\ BufCapacity = 3 ASSUME Assumption == /\ Producers # {} ( at least one producer ) /\ Consumers # {} ( at least one consumer ) /\ Producers \intersect Consumers = {} ( no thread is both consumer and producer ) /\ BufCapacity \in (Nat \ {0}) ( buffer capacity is at least 1 )

---

VARIABLES buffer, waitSet vars == <<buffer, waitSet>>

RunningThreads == (Producers \cup Consumers) \ waitSet ( @see java.lang.Object#notify ) Notify == IF waitSet # ({} <: {STRING}) * {} THEN \E x \in waitSet: waitSet' = waitSet \ {x} ELSE UNCHANGED waitSet ( @see java.lang.Object#wait ) Wait(t) == /\ waitSet' = waitSet \cup {t} /\ UNCHANGED <>

---

Put(t, d) == \/ /\ Len(buffer) < BufCapacity /\ buffer' = Append(buffer, d) /\ Notify \/ /\ Len(buffer) = BufCapacity /\ Wait(t)

Get(t) == \/ /\ buffer # <<>> <: Seq(STRING) * <<>> /\ buffer' = Tail(buffer) /\ Notify \/ /\ buffer = <<>> <: Seq(STRING) * /\ Wait(t)

---

( Initially, the buffer is empty and no thread is waiting. ) Init == /\ buffer = (<<>> <: Seq(STRING)) /\ waitSet = ({} <: {STRING}) ( Then, pick a thread out of all running threads and have it do its thing. ) Next == \E t \in RunningThreads: \/ /\ t \in Producers /\ Put(t, t) * Add some data to buffer \/ /\ t \in Consumers /\ Get(t)

Invariant == waitSet # (Producers \cup Consumers) CONSTANTS c3, p1, p2, p3, p4, c1, c2 * TRACE Sub-Action definition 0 Next_sa_0 == ( /\ buffer = (<<>>) /\ waitSet = ({}) /\ buffer' = (<>) /\ waitSet' = ({}) ) * TRACE Sub-Action definition 1 Next_sa_1 == ( /\ buffer = (<>) /\ waitSet = ({}) /\ buffer' = (<<p1, p1>>) /\ waitSet' = ({}) ) * TRACE Sub-Action definition 2 Next_sa_2 == ( /\ buffer = (<<p1, p1>>) /\ waitSet = ({}) /\ buffer' = (<<p1, p1, p1>>) /\ waitSet' = ({}) ) * TRACE Sub-Action definition 3 Next_sa_3 == ( /\ buffer = (<<p1, p1, p1>>) /\ waitSet = ({}) /\ buffer' = (<<p1, p1, p1>>) /\ waitSet' = ({p1}) ) * TRACE Sub-Action definition 4 Next_sa_4 == ( /\ buffer = (<<p1, p1, p1>>) /\ waitSet = ({p1}) /\ buffer' = (<<p1, p1, p1>>) /\ waitSet' = ({p1, p2}) ) * TRACE Sub-Action definition 5 Next_sa_5 == ( /\ buffer = (<<p1, p1, p1>>) /\ waitSet = ({p1, p2}) /\ buffer' = (<<p1, p1, p1>>) /\ waitSet' = ({p1, p2, p3}) ) * TRACE Sub-Action definition 6 Next_sa_6 == ( /\ buffer = (<<p1, p1, p1>>) /\ waitSet = ({p1, p2, p3}) /\ buffer' = (<<p1, p1, p1>>) /\ waitSet' = ({p1, p2, p3, p4}) ) * TRACE Sub-Action definition 7 Next_sa_7 == ( /\ buffer = (<<p1, p1, p1>>) /\ waitSet = ({p1, p2, p3, p4}) /\ buffer' = (<<p1, p1>>) /\ waitSet' = ({p2, p3, p4}) ) * TRACE Sub-Action definition 8 Next_sa_8 == ( /\ buffer = (<<p1, p1>>) /\ waitSet = ({p2, p3, p4}) /\ buffer' = (<>) /\ waitSet' = ({p3, p4}) ) * TRACE Sub-Action definition 9 Next_sa_9 == ( /\ buffer = (<>) /\ waitSet = ({p3, p4}) /\ buffer' = (<<>>) /\ waitSet' = ({p4}) ) * TRACE Sub-Action definition 10 Next_sa_10 == ( /\ buffer = (<<>>) /\ waitSet = ({p4}) /\ buffer' = (<<>>) /\ waitSet' = ({p4, c1}) ) * TRACE Sub-Action definition 11 Next_sa_11 == ( /\ buffer = (<<>>) /\ waitSet = ({p4, c1}) /\ buffer' = (<<>>) /\ waitSet' = ({p4, c1, c2}) ) * TRACE Sub-Action definition 12 Next_sa_12 == ( /\ buffer = (<<>>) /\ waitSet = ({p4, c1, c2}) /\ buffer' = (<<>>) /\ waitSet' = ({p4, c1, c2, c3}) ) * TRACE Sub-Action definition 13 Next_sa_13 == ( /\ buffer = (<<>>) /\ waitSet = ({p4, c1, c2, c3}) /\ buffer' = (<>) /\ waitSet' = ({c1, c2, c3}) ) * TRACE Sub-Action definition 14 Next_sa_14 == ( /\ buffer = (<>) /\ waitSet = ({c1, c2, c3}) /\ buffer' = (<<p1, p1>>) /\ waitSet' = ({c2, c3}) ) * TRACE Sub-Action definition 15 Next_sa_15 == ( /\ buffer = (<<p1, p1>>) /\ waitSet = ({c2, c3}) /\ buffer' = (<<p1, p1, p1>>) /\ waitSet' = ({c3}) ) * TRACE Sub-Action definition 16 Next_sa_16 == ( /\ buffer = (<<p1, p1, p1>>) /\ waitSet = ({c3}) /\ buffer' = (<<p1, p1, p1>>) /\ waitSet' = ({p1, c3}) ) * TRACE Sub-Action definition 17 Next_sa_17 == ( /\ buffer = (<<p1, p1, p1>>) /\ waitSet = ({p1, c3}) /\ buffer' = (<<p1, p1, p1>>) /\ waitSet' = ({p1, p2, c3}) ) * TRACE Sub-Action definition 18 Next_sa_18 == ( /\ buffer = (<<p1, p1, p1>>) /\ waitSet = ({p1, p2, c3}) /\ buffer' = (<<p1, p1, p1>>) /\ waitSet' = ({p1, p2, p3, c3}) ) * TRACE Sub-Action definition 19 Next_sa_19 == ( /\ buffer = (<<p1, p1, p1>>) /\ waitSet = ({p1, p2, p3, c3}) /\ buffer' = (<<p1, p1, p1>>) /\ waitSet' = ({p1, p2, p3, p4, c3}) ) * TRACE Sub-Action definition 20 Next_sa_20 == ( /\ buffer = (<<p1, p1, p1>>) /\ waitSet = ({p1, p2, p3, p4, c3}) /\ buffer' = (<<p1, p1>>) /\ waitSet' = ({p2, p3, p4, c3}) ) * TRACE Sub-Action definition 21 Next_sa_21 == ( /\ buffer = (<<p1, p1>>) /\ waitSet = ({p2, p3, p4, c3}) /\ buffer' = (<>) /\ waitSet' = ({p3, p4, c3}) ) * TRACE Sub-Action definition 22 Next_sa_22 == ( /\ buffer = (<>) /\ waitSet = ({p3, p4, c3}) /\ buffer' = (<<>>) /\ waitSet' = ({p3, p4}) ) * TRACE Sub-Action definition 23 Next_sa_23 == ( /\ buffer = (<<>>) /\ waitSet = ({p3, p4}) /\ buffer' = (<<>>) /\ waitSet' = ({p3, p4, c1}) ) * TRACE Sub-Action definition 24 Next_sa_24 == ( /\ buffer = (<<>>) /\ waitSet = ({p3, p4, c1}) /\ buffer' = (<<>>) /\ waitSet' = ({p3, p4, c1, c2}) ) * TRACE Sub-Action definition 25 Next_sa_25 == ( /\ buffer = (<<>>) /\ waitSet = ({p3, p4, c1, c2}) /\ buffer' = (<<>>) /\ waitSet' = ({p3, p4, c1, c2, c3}) ) * TRACE Sub-Action definition 26 Next_sa_26 == ( /\ buffer = (<<>>) /\ waitSet = ({p3, p4, c1, c2, c3}) /\ buffer' = (<>) /\ waitSet' = ({p4, c1, c2, c3}) ) * TRACE Sub-Action definition 27 Next_sa_27 == ( /\ buffer = (<>) /\ waitSet = ({p4, c1, c2, c3}) /\ buffer' = (<<p1, p1>>) /\ waitSet' = ({c1, c2, c3}) ) * TRACE Sub-Action definition 28 Next_sa_28 == ( /\ buffer = (<<p1, p1>>) /\ waitSet = ({c1, c2, c3}) /\ buffer' = (<<p1, p1, p1>>) /\ waitSet' = ({c2, c3}) ) * TRACE Sub-Action definition 29 Next_sa_29 == ( /\ buffer = (<<p1, p1, p1>>) /\ waitSet = ({c2, c3}) /\ buffer' = (<<p1, p1, p1>>) /\ waitSet' = ({p1, c2, c3}) ) * TRACE Sub-Action definition 30 Next_sa_30 == ( /\ buffer = (<<p1, p1, p1>>) /\ waitSet = ({p1, c2, c3}) /\ buffer' = (<<p1, p1, p1>>) /\ waitSet' = ({p1, p2, c2, c3}) ) * TRACE Sub-Action definition 31 Next_sa_31 == ( /\ buffer = (<<p1, p1, p1>>) /\ waitSet = ({p1, p2, c2, c3}) /\ buffer' = (<<p1, p1, p1>>) /\ waitSet' = ({p1, p2, p3, c2, c3}) ) * TRACE Sub-Action definition 32 Next_sa_32 == ( /\ buffer = (<<p1, p1, p1>>) /\ waitSet = ({p1, p2, p3, c2, c3}) /\ buffer' = (<<p1, p1, p1>>) /\ waitSet' = ({p1, p2, p3, p4, c2, c3}) ) * TRACE Sub-Action definition 33 Next_sa_33 == ( /\ buffer = (<<p1, p1, p1>>) /\ waitSet = ({p1, p2, p3, p4, c2, c3}) /\ buffer' = (<<p1, p1>>) /\ waitSet' = ({p2, p3, p4, c2, c3}) ) * TRACE Sub-Action definition 34 Next_sa_34 == ( /\ buffer = (<<p1, p1>>) /\ waitSet = ({p2, p3, p4, c2, c3}) /\ buffer' = (<>) /\ waitSet' = ({p2, p3, p4, c3}) ) * TRACE Sub-Action definition 35 Next_sa_35 == ( /\ buffer = (<>) /\ waitSet = ({p2, p3, p4, c3}) /\ buffer' = (<<>>) /\ waitSet' = ({p2, p3, p4}) ) * TRACE Sub-Action definition 36 Next_sa_36 == ( /\ buffer = (<<>>) /\ waitSet = ({p2, p3, p4}) /\ buffer' = (<<>>) /\ waitSet' = ({p2, p3, p4, c1}) ) * TRACE Sub-Action definition 37 Next_sa_37 == ( /\ buffer = (<<>>) /\ waitSet = ({p2, p3, p4, c1}) /\ buffer' = (<<>>) /\ waitSet' = ({p2, p3, p4, c1, c2}) ) * TRACE Sub-Action definition 38 Next_sa_38 == ( /\ buffer = (<<>>) /\ waitSet = ({p2, p3, p4, c1, c2}) /\ buffer' = (<<>>) /\ waitSet' = ({p2, p3, p4, c1, c2, c3}) ) * TRACE Sub-Action definition 39 Next_sa_39 == ( /\ buffer = (<<>>) /\ waitSet = ({p2, p3, p4, c1, c2, c3}) /\ buffer' = (<>) /\ waitSet' = ({p3, p4, c1, c2, c3}) ) * TRACE Sub-Action definition 40 Next_sa_40 == ( /\ buffer = (<>) /\ waitSet = ({p3, p4, c1, c2, c3}) /\ buffer' = (<<p1, p1>>) /\ waitSet' = ({p4, c1, c2, c3}) ) * TRACE Sub-Action definition 41 Next_sa_41 == ( /\ buffer = (<<p1, p1>>) /\ waitSet = ({p4, c1, c2, c3}) /\ buffer' = (<<p1, p1, p1>>) /\ waitSet' = ({c1, c2, c3}) ) * TRACE Sub-Action definition 42 Next_sa_42 == ( /\ buffer = (<<p1, p1, p1>>) /\ waitSet = ({c1, c2, c3}) /\ buffer' = (<<p1, p1, p1>>) /\ waitSet' = ({p1, c1, c2, c3}) ) * TRACE Sub-Action definition 43 Next_sa_43 == ( /\ buffer = (<<p1, p1, p1>>) /\ waitSet = ({p1, c1, c2, c3}) /\ buffer' = (<<p1, p1, p1>>) /\ waitSet' = ({p1, p2, c1, c2, c3}) ) * TRACE Sub-Action definition 44 Next_sa_44 == ( /\ buffer = (<<p1, p1, p1>>) /\ waitSet = ({p1, p2, c1, c2, c3}) /\ buffer' = (<<p1, p1, p1>>) /\ waitSet' = ({p1, p2, p3, c1, c2, c3}) ) * TRACE Action Constraint definition traceExploreActionConstraint _SpecTEActionConstraint ==<< Next_sa_0, Next_sa_1, Next_sa_2, Next_sa_3, Next_sa_4, Next_sa_5, Next_sa_6, Next_sa_7, Next_sa_8, Next_sa_9, Next_sa_10, Next_sa_11, Next_sa_12, Next_sa_13, Next_sa_14, Next_sa_15, Next_sa_16, Next_sa_17, Next_sa_18, Next_sa_19, Next_sa_20, Next_sa_21, Next_sa_22, Next_sa_23, Next_sa_24, Next_sa_25, Next_sa_26, Next_sa_27, Next_sa_28, Next_sa_29, Next_sa_30, Next_sa_31, Next_sa_32, Next_sa_33, Next_sa_34, Next_sa_35, Next_sa_36, Next_sa_37, Next_sa_38, Next_sa_39, Next_sa_40, Next_sa_41, Next_sa_42, Next_sa_43, Next_sa_44>>[TLCGet("level")]

def_ov_15810930190442000 == << ([buffer |-> <<>>,waitSet |-> {}]), ([buffer |-> <>,waitSet |-> {}]), ([buffer |-> <<p1, p1>>,waitSet |-> {}]), ([buffer |-> <<p1, p1, p1>>,waitSet |-> {}]), ([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1}]), ([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2}]), ([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2, p3}]), ([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2, p3, p4}]), ([buffer |-> <<p1, p1>>,waitSet |-> {p2, p3, p4}]), ([buffer |-> <>,waitSet |-> {p3, p4}]), ([buffer |-> <<>>,waitSet |-> {p4}]), ([buffer |-> <<>>,waitSet |-> {p4, c1}]), ([buffer |-> <<>>,waitSet |-> {p4, c1, c2}]), ([buffer |-> <<>>,waitSet |-> {p4, c1, c2, c3}]), ([buffer |-> <>,waitSet |-> {c1, c2, c3}]), ([buffer |-> <<p1, p1>>,waitSet |-> {c2, c3}]), ([buffer |-> <<p1, p1, p1>>,waitSet |-> {c3}]), ([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, c3}]), ([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2, c3}]), ([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2, p3, c3}]), ([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2, p3, p4, c3}]), ([buffer |-> <<p1, p1>>,waitSet |-> {p2, p3, p4, c3}]), ([buffer |-> <>,waitSet |-> {p3, p4, c3}]), ([buffer |-> <<>>,waitSet |-> {p3, p4}]), ([buffer |-> <<>>,waitSet |-> {p3, p4, c1}]), ([buffer |-> <<>>,waitSet |-> {p3, p4, c1, c2}]), ([buffer |-> <<>>,waitSet |-> {p3, p4, c1, c2, c3}]), ([buffer |-> <>,waitSet |-> {p4, c1, c2, c3}]), ([buffer |-> <<p1, p1>>,waitSet |-> {c1, c2, c3}]), ([buffer |-> <<p1, p1, p1>>,waitSet |-> {c2, c3}]), ([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, c2, c3}]), ([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2, c2, c3}]), ([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2, p3, c2, c3}]), ([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2, p3, p4, c2, c3}]), ([buffer |-> <<p1, p1>>,waitSet |-> {p2, p3, p4, c2, c3}]), ([buffer |-> <>,waitSet |-> {p2, p3, p4, c3}]), ([buffer |-> <<>>,waitSet |-> {p2, p3, p4}]), ([buffer |-> <<>>,waitSet |-> {p2, p3, p4, c1}]), ([buffer |-> <<>>,waitSet |-> {p2, p3, p4, c1, c2}]), ([buffer |-> <<>>,waitSet |-> {p2, p3, p4, c1, c2, c3}]), ([buffer |-> <>,waitSet |-> {p3, p4, c1, c2, c3}]), ([buffer |-> <<p1, p1>>,waitSet |-> {p4, c1, c2, c3}]), ([buffer |-> <<p1, p1, p1>>,waitSet |-> {c1, c2, c3}]), ([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, c1, c2, c3}]), ([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2, c1, c2, c3}]), ([buffer |-> <<p1, p1, p1>>,waitSet |-> {p1, p2, p3, c1, c2, c3}])>>

* VARIABLE TraceExp * TRACE INIT definition traceExploreInit _SpecTEInit == /\ buffer = ( <<>> ) /\ waitSet = ( {} )* /\ TraceExp = TRUE

---

* TRACE NEXT definition traceExploreNext _SpecTENext ==/\ \/ Next_sa_0 \/ Next_sa_1 \/ Next_sa_2 \/ Next_sa_3 \/ Next_sa_4 \/ Next_sa_5 \/ Next_sa_6 \/ Next_sa_7 \/ Next_sa_8 \/ Next_sa_9 \/ Next_sa_10 \/ Next_sa_11 \/ Next_sa_12 \/ Next_sa_13 \/ Next_sa_14 \/ Next_sa_15 \/ Next_sa_16 \/ Next_sa_17 \/ Next_sa_18 \/ Next_sa_19 \/ Next_sa_20 \/ Next_sa_21 \/ Next_sa_22 \/ Next_sa_23 \/ Next_sa_24 \/ Next_sa_25 \/ Next_sa_26 \/ Next_sa_27 \/ Next_sa_28 \/ Next_sa_29 \/ Next_sa_30 \/ Next_sa_31 \/ Next_sa_32 \/ Next_sa_33 \/ Next_sa_34 \/ Next_sa_35 \/ Next_sa_36 \/ Next_sa_37 \/ Next_sa_38 \/ Next_sa_39 \/ Next_sa_40 \/ Next_sa_41 \/ Next_sa_42 \/ Next_sa_43 \/ Next_sa_44* /\ TraceExp' = TraceExp

=============================================================================

out-parser-json.txt https://github.com/konnov/apalache/files/4172787/out-parser-json.txt

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/konnov/apalache/issues/77?email_source=notifications&email_token=AOF3ZPUA6VLMIBURYBMO5BLRBW7A5A5CNFSM4JXNTQK2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOELEPCAA#issuecomment-583594240, or unsubscribe https://github.com/notifications/unsubscribe-auth/AOF3ZPTNZE5VFF3LUDJNIIDRBW7A5ANCNFSM4JXNTQKQ .

[konnov]

A few apalache modules need z3 to be compiled. However, the JSON exporter should depend only on the module tlair, which does not use z3 and is not going to be dynamically linked against z3.

[andrey-kuprianov]

implemented with the last commit 73dddd96b99f3d17965741ced0ec532d95576106