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

Spec that extends TLAPS causes at.forsyte.apalache.tla.imp.SanyImporterException #89

Closed lemmy closed 4 years ago

lemmy commented 4 years ago 
------------------------- MODULE Apalache -------------------------

a <: b == a

===================================================================
--------------------------- MODULE BlockingQueue ---------------------------
EXTENDS Naturals, Sequences, FiniteSets, Apalache

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 # ({} <: {STRING})
             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 # <<>> <: Seq(STRING)
      /\ buffer' = Tail(buffer)
      /\ NotifyOther(t)
   \/ /\ 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 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 OBVIOUS 
<1>2. TypeInv /\ [Next]_vars => TypeInv' OBVIOUS 
<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 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)

=============================================================================
markus@avocado:~/src/TLA/models/tutorials/BlockingQueueTLA(master)$ ~/src/TLA/_community/apalache/bin/apalache-mc check --init=Init --cinit=ConstInit --next=Next --length=7 --inv=Inv --nworkers=4 --debug BlockingQueue.tla
# Tool home: /home/markus/src/TLA/_community/apalache
# Package:   /home/markus/src/TLA/_community/apalache/apalache-pkg-0.6.0-SNAPSHOT-full.jar
# JVM args: -Xmx4096m
#
# APALACHE version 0.6.0-SNAPSHOT build 0.5.0-289-gab39edc
#
# WARNING: This tool is in the experimental stage.
#          Please report bugs at: [https://github.com/konnov/apalache/issues]

Checker options: filename=BlockingQueue.tla, init=Init, next=Next, inv=Inv I@211935.806
WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by com.google.inject.internal.cglib.core.$ReflectUtils$1 (file:/home/markus/src/TLA/_community/apalache/apalache-pkg-0.6.0-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@211936.593
Parsing file /home/markus/src/TLA/_specs/models/tutorials/BlockingQueueTLA/BlockingQueue.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/Sequences.tla
Parsing file /tmp/FiniteSets.tla
Parsing file /home/markus/src/TLA/_specs/models/tutorials/BlockingQueueTLA/Apalache.tla
Parsing file /home/markus/src/TLA/_specs/models/tutorials/BlockingQueueTLA/TLAPS.tla
(This should not have happened, but it did. REPORT IT: [https://github.com/konnov/apalache/issues],at.forsyte.apalache.tla.imp.SanyImporterException: Unsupported operator: $Nop)
Unhandled exception                                                 E@211937.130
at.forsyte.apalache.tla.imp.SanyImporterException: Unsupported operator: $Nop
    at at.forsyte.apalache.tla.imp.OpApplTranslator.translateBuiltin(OpApplTranslator.scala:200)
    at at.forsyte.apalache.tla.imp.OpApplTranslator.translate(OpApplTranslator.scala:44)
    at at.forsyte.apalache.tla.imp.ExprOrOpArgNodeTranslator.translate(ExprOrOpArgNodeTranslator.scala:33)
    at at.forsyte.apalache.tla.imp.OpApplTranslator.$anonfun$translateBuiltin$1(OpApplTranslator.scala:156)
    at scala.collection.immutable.List.map(List.scala:286)
    at at.forsyte.apalache.tla.imp.OpApplTranslator.translateBuiltin(OpApplTranslator.scala:156)
    at at.forsyte.apalache.tla.imp.OpApplTranslator.translate(OpApplTranslator.scala:44)
    at at.forsyte.apalache.tla.imp.ExprOrOpArgNodeTranslator.translate(ExprOrOpArgNodeTranslator.scala:33)
    at at.forsyte.apalache.tla.imp.OpDefTranslator.translate(OpDefTranslator.scala:37)
    at at.forsyte.apalache.tla.imp.ModuleTranslator.eachOpDefSecondPass$1(ModuleTranslator.scala:56)
    at at.forsyte.apalache.tla.imp.ModuleTranslator.$anonfun$translate$4(ModuleTranslator.scala:64)
    at at.forsyte.apalache.tla.imp.ModuleTranslator.$anonfun$translate$4$adapted(ModuleTranslator.scala:64)
    at scala.collection.immutable.List.foreach(List.scala:392)
    at at.forsyte.apalache.tla.imp.ModuleTranslator.translate(ModuleTranslator.scala:64)
    at at.forsyte.apalache.tla.imp.SanyImporter.$anonfun$loadFromFile$1(SanyImporter.scala:39)
    at scala.collection.IndexedSeqOptimized.foldLeft(IndexedSeqOptimized.scala:60)
    at scala.collection.IndexedSeqOptimized.foldLeft$(IndexedSeqOptimized.scala:68)
    at scala.collection.mutable.ArrayOps$ofRef.foldLeft(ArrayOps.scala:198)
    at at.forsyte.apalache.tla.imp.SanyImporter.loadFromFile(SanyImporter.scala:38)
    at at.forsyte.apalache.tla.imp.passes.SanyParserPassImpl.execute(SanyParserPassImpl.scala:42)
    at at.forsyte.apalache.infra.passes.PassChainExecutor.exec$1(PassChainExecutor.scala:23)
    at at.forsyte.apalache.infra.passes.PassChainExecutor.run(PassChainExecutor.scala:38)
    at at.forsyte.apalache.tla.Tool$.runCheck(Tool.scala:119)
    at at.forsyte.apalache.tla.Tool$.$anonfun$main$2(Tool.scala:57)
    at at.forsyte.apalache.tla.Tool$.$anonfun$main$2$adapted(Tool.scala:57)
    at at.forsyte.apalache.tla.Tool$.handleExceptions(Tool.scala:168)
    at at.forsyte.apalache.tla.Tool$.main(Tool.scala:57)
    at at.forsyte.apalache.tla.Tool.main(Tool.scala)
konnov commented 4 years ago

That was actually easy. The problematic expression was TypeInv!2, which produced a $Nop. This is now translated to NullEx.