search

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint
https://apalache-mc.org/
Apache License 2.0
440 stars 40 forks source link

[BUG] Could not parse TLC configuration in BlockingQueue.cfg: string matching regex '\z' expected but '{' found #208

Closed lemmy closed 3 years ago

lemmy commented 4 years ago 
kuppe@mkuppe-z440:~/src/TLA/blockingqueue$ ../apalache/bin/apalache-mc check BlockingQueue.tla
# Tool home: /home/mkuppe/src/TLA/apalache
# Package:   /home/mkuppe/src/TLA/apalache/mod-distribution/target/apalache-pkg-0.7.3-SNAPSHOT-full.jar
# JVM args: -Xmx4096m -Djava.library.path=/home/mkuppe/src/TLA/apalache/3rdparty/lib  -DTLA-Library=/home/mkuppe/src/TLA/apalache/src/tla:/home/mkuppe/src/TLA/blockingqueue/
#
# APALACHE version 0.7.3-SNAPSHOT build v0.7.0-28-gdd171c8
#
# WARNING: This tool is in the experimental stage.
#          Please report bugs at: [https://github.com/informalsystems/apalache/issues]

Checker options: filename=BlockingQueue.tla, init=, next=, inv=   I@19:04:13.850
WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by com.google.inject.internal.cglib.core.$ReflectUtils$1 (file:/home/mkuppe/src/TLA/apalache/mod-distribution/target/apalache-pkg-0.7.3-SNAPSHOT-full.jar) to method java.lang.ClassLoader.defineClass(java.lang.String,byte[],int,int,java.security.ProtectionDomain)
WARNING: Please consider reporting this to the maintainers of com.google.inject.internal.cglib.core.$ReflectUtils$1
WARNING: Use --illegal-access=warn to enable warnings of further illegal reflective access operations
WARNING: All illegal access operations will be denied in a future release
PASS #0: SanyParser                                               I@19:04:14.139
Parsing file /home/mkuppe/src/TLA/blockingqueue/BlockingQueue.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/Sequences.tla
Parsing file /tmp/FiniteSets.tla
Parsing file /home/mkuppe/src/TLA/blockingqueue/TLAPS.tla
PASS #1: ConfigurationPass                                        I@19:04:14.482
  > Loading TLC configuration from BlockingQueue.cfg              I@19:04:14.483
Configuration error (see the manual):   > Could not parse TLC configuration in BlockingQueue.cfg: string matching regex '\z' expected but '{' found E@19:04:14.523
It took me 0 days  0 hours  0 min  0 sec                          I@19:04:14.524
Total time: 0.727 sec                                             I@19:04:14.524
EXITCODE: ERROR (99)

mkuppe@mkuppe-z440:~/src/TLA/blockingqueue$ cat BlockingQueue.cfg 
\* SPECIFICATION
CONSTANTS
    BufCapacity = 3
    Producers = {p1,p2,p3,p4}
    Consumers = {c1,c2,c3}

SPECIFICATION FairSpec

INVARIANT Invariant
INVARIANT TypeInv

PROPERTY Starvation

mkuppe@mkuppe-z440:~/src/TLA/blockingqueue$ uname -a
Linux mkuppe-z440 5.4.0-42-generic #46-Ubuntu SMP Fri Jul 10 00:24:02 UTC 2020 x86_64 x86_64 x86_64 GNU/Linux

mkuppe@mkuppe-z440:~/src/TLA/blockingqueue$ java -version
openjdk version "11.0.8" 2020-07-14
OpenJDK Runtime Environment (build 11.0.8+10-post-Ubuntu-0ubuntu120.04)
OpenJDK 64-Bit Server VM (build 11.0.8+10-post-Ubuntu-0ubuntu120.04, mixed mode, sharing)
--------------------------- MODULE BlockingQueue ---------------------------
EXTENDS Naturals, Sequences, FiniteSets

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

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

NotifyOther(t) == 
          LET S == IF t \in Producers THEN waitSet \ Producers ELSE waitSet \ Consumers
          IN IF S # {}
             THEN \E x \in S : waitSet' = waitSet \ {x}
             ELSE UNCHANGED waitSet

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

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

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

Get(t) ==
/\ t \notin waitSet
/\ \/ /\ buffer # <<>>
      /\ buffer' = Tail(buffer)
      /\ NotifyOther(t)
   \/ /\ buffer = <<>>
      /\ Wait(t)

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

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

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

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

(* TLA+ is untyped, thus lets verify the range of some values in each state. *)
TypeInv == /\ buffer \in Seq(Producers)
           /\ Len(buffer) \in 0..BufCapacity
           /\ waitSet \in SUBSET (Producers \cup Consumers)

(* No Deadlock *)
Invariant == waitSet # (Producers \cup Consumers)

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

MySeq(P) == UNION {[1..n -> P] : n \in 0..BufCapacity}

INSTANCE TLAPS

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

(* Whitelist all the known facts and definitions (except IInv below) *)
USE Assumption DEF vars, RunningThreads,
                   Init, Next, Spec,
                   Put, Get,
                   Wait, NotifyOther,
                   TypeInv, Invariant

\* TypeInv will be a conjunct of the inductive invariant, so prove it inductive.
\* An invariant I is inductive, iff Init => I and I /\ [Next]_vars => I. Note
\* though, that TypeInv itself won't imply Invariant though!  TypeInv alone
\* does not help us prove Invariant.
\* Luckily, TLAPS does not require us to decompose the proof into substeps. 
LEMMA TypeCorrect == Spec => []TypeInv
<1>1. Init => TypeInv BY SMT 
<1>2. TypeInv /\ [Next]_vars => TypeInv' BY SMT 
<1>. QED BY <1>1, <1>2, PTL

\* The naive thing to do is to check if the conjunct of TypeInv /\ Invariant
\* is inductive.
IInv == /\ TypeInv!2
        /\ TypeInv!3
        /\ Invariant
        \* When the buffer is empty, a consumer will be added to the waitSet.
        \* However, this does not crate a deadlock, because at least one producer
        \* will not be in the waitSet.
        /\ buffer = <<>> => \E p \in Producers : p \notin waitSet
        \* Vice versa, when buffer is full, a producer will be added to waitSet,
        \* but at least one consumer won't be in waitSet.
        /\ Len(buffer) = BufCapacity => \E c \in Consumers : c \notin waitSet

THEOREM DeadlockFreedom == Spec => []Invariant
<1>1. Init => IInv BY SMT DEF IInv
<1>2. IInv /\ [Next]_vars => IInv' BY DEF IInv
<1>3. IInv => Invariant  BY DEF IInv
<1>4. QED BY <1>1,<1>2,<1>3,PTL

MCIInv == TypeInv!1 /\ IInv

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

PutEnabled == \A p \in Producers : ENABLED Put(p, p)

FairSpec == Spec /\ WF_vars(Next) 
                 /\ \A p \in Producers : WF_vars(Put(p, p)) 

(* All producers will continuously be serviced. For this to be violated,    *)
(* ASSUME Cardinality(Producers) > 1 has to hold (a single producer cannot  *)
(* starve itself).                                                          *)
Starvation == \A p \in Producers: []<>(<<Put(p, p)>>_vars)

=============================================================================
shonfeder commented 4 years ago

Just some notes as I use this bug report as an opportunity to dig into the code a bit.

So here's the error being raised:

https://github.com/informalsystems/apalache/blob/dd171c8417b7ec651b6116abe2261f2c9abc9406/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/ConfigurationPassImpl.scala#L128-L130

I suspect it's coming from this part of the lexer:

https://github.com/informalsystems/apalache/blob/dd171c8417b7ec651b6116abe2261f2c9abc9406/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/config/TlcConfigLexer.scala#L28-L41

After including the parser location in the error message, it became clear the parser is failing on the last line here, at the opening {:

\* SPECIFICATION
CONSTANTS
    BufCapacity = 3
    Producers = {p1,p2,p3,p4}

(See https://github.com/lemmy/BlockingQueue/blob/3a66f46f6f5703f2863f71baaf0aedaaee58836f/BlockingQueue.cfg#L1-L4 for the source.)

Indeed, the lexer defined in TlcConfigLexer.scala is not equipped to recognize sets at all. Presumably this pertains to the "limited syntax" noted in the manual https://github.com/informalsystems/apalache/blob/unstable/docs/manual.md#54-tlc-configuration-file ?

If this is currently a necessary limitation, then we can at least improve the documentation and the error reporting to help guide the user. If this is not a necessary limitation, I'd be interested in adding the support for handling sets in cfg files.

lemmy commented 4 years ago

Why wasn't it possible to reuse TLC's config parser?

konnov commented 4 years ago

Our conjecture was that the users are not writing .cfg files by hand. Rather they use whatever is produced by the TLA+ Toolbox. This obviously does not apply to the power users :-)

It looks to me that the ability to define sets in .cfg is redundant, as one can do that directly in TLA+. That is what TLA+ Toolbox is doing, right?

konnov commented 4 years ago

@lemmy, could you point us to the TLC's config parser, so we could evaluate the efforts of integrating with it?

lemmy commented 4 years ago

The VScode extension that appears to be popular, especially amongst new users, requires users to write the config file by hand. I believe it's considered a feature.

tlc2.tool.impl.ModelConfig (it has few dependencies)

konnov commented 3 years ago

@lemmy, I am looking at ModelConfig right now. The following statements are not specified in Leslie's book:

Are they documented anywhere? I can guess what CHECK_DEADLOCK is supposed to mean, but what about the other two?

lemmy commented 3 years ago

I find ALIAS to be really useful (to e.g. do trace expressions).

konnov commented 3 years ago

I guess, ALIAS is supposed to be similar to alias in shell? From what I see in the description, it is more like DISPLAY or SHOW. But if it is already in production, that is not important.

lemmy commented 3 years ago

ALIAS is actually inspired by SQL's ALIAS, but VIEW would have been the best term. Unfortunately, VIEW was already taken.