This project is read-only.
1

Closed

Trace Exploration error when extending WellFoundedInduction

description

I have a module Plumtree which extends another module, Network. While attempting to investigate a temporal-property violation I tried to explore an expression, commChannels[2,1], and got an error:

Error(s) from running the Trace Explorer:
TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException: Attempted to check equality of integer 0 with non-integer:
[msrc |-> 3, mtype |-> "Gossip", mid |-> 0, mbody |-> b1]
Error(s) from running the Trace Explorer:
The error occurred when TLC was evaluating the nested
expressions at the following positions:
  1. Line 530, column 3 to line 619, column 1 in TE
  2. Line 530, column 3 to line 603, column 1 in TE
  3. Line 530, column 3 to line 600, column 1 in TE
  4. Line 530, column 3 to line 597, column 1 in TE
  5. Line 530, column 3 to line 594, column 1 in TE
  6. Line 530, column 3 to line 591, column 1 in TE
  7. Line 530, column 3 to line 588, column 1 in TE
  8. Line 530, column 3 to line 585, column 1 in TE
  9. Line 530, column 3 to line 580, column 1 in TE
  10. Line 530, column 3 to line 577, column 1 in TE
  11. Line 530, column 3 to line 574, column 1 in TE
  12. Line 530, column 3 to line 558, column 1 in TE
  13. Line 530, column 3 to line 555, column 1 in TE
  14. Line 530, column 3 to line 552, column 1 in TE
  15. Line 530, column 3 to line 549, column 1 in TE
  16. Line 530, column 3 to line 546, column 1 in TE
  17. Line 530, column 3 to line 543, column 1 in TE
  18. Line 530, column 3 to line 540, column 1 in TE
  19. Line 530, column 3 to line 535, column 1 in TE
  20. Line 530, column 3 to line 532, column 1 in TE
  21. Line 533, column 2 to line 535, column 1 in TE
  22. Line 536, column 2 to line 540, column 1 in TE
Removing WellFoundedInduction from the extended module (below) solves the problem.


------------------------------ MODULE Network ------------------------------
EXTENDS Integers, Sequences, TLAPS, NaturalsInduction, WellFoundedInduction

CONSTANT Peer
CONSTANT Nil
CONSTANT Msg

* For testing - maximum amount of messages to send
CONSTANT MAX_MSG

ASSUME /\ Peer \subseteq Nat
   /\ Nil \in Nat \ Peer
   /\ MAX_MSG \in Nat
VARIABLES commChannels

* For testing - message counter
VARIABLE msgCounter

netvars == << commChannels, msgCounter >>


Receive(to, from) == /\ commChannels' = [commChannels EXCEPT ![from, to] =
                                        [commChannels[from, to] EXCEPT
                                                      !.out = Append(@, Head(commChannels[from, to].in)),
                                                      !.in  = Tail(@)]]
                 /\ UNCHANGED << msgCounter >>
Send(m, from, to) == commChannels' = [commChannels EXCEPT ![from, to] =
                                       [commChannels[from, to] EXCEPT !.in = Append(commChannels[from, to].in, m)]]

HasMsg(i, j) == Len(commChannels[j, i].in) > 0

Comm(self) == \/ /\ msgCounter < MAX_MSG
             /\ \E m \in Msg, p \in Peer: Send(m, self, p)
             /\ msgCounter' = msgCounter + 1
          \/ \E p \in Peer: /\ Len(commChannels[p, self].in) > 0
                            /\ Receive(self, p)

NWInit == /\ commChannels = [peer1 \in Peer, peer2 \in Peer |->
                                         [in |-> <<>>, out |-> <<>>] ]
      /\ msgCounter = 0
NWNext == \/ (\E self \in Peer: Comm(self))
      \/ (* Disjunct to prevent deadlock on termination *)
         /\ msgCounter = MAX_MSG
         /\ \A p1 \in Peer, p2 \in Peer: Len(commChannels[p1, p2].in) = 0
         /\ UNCHANGED netvars
NWSpec == /\ NWInit /\ [][NWNext]_netvars
      /\ \A self \in Peer : WF_netvars(Comm(self))


NWTypeOK == /\ msgCounter \in Nat
        /\ \A p1 \in Peer, p2 \in Peer: /\ commChannels[p1, p2].in \in Seq(Msg) 
                                        /\ commChannels[p1, p2].out \in Seq(Msg)
LEMMA NWInit => NWTypeOK
<1>1. SUFFICES ASSUME NWInit
           PROVE NWTypeOK
OBVIOUS
<1>2. QED
BY DEF Nat, NWInit, NWTypeOK


Count[i \in Peer, P \in SUBSET Peer] == IF P = {} THEN 0
                                    ELSE LET j == CHOOSE p \in P: TRUE 
                                         IN Len(commChannels[i, j].out) + 
                                            Count[i, P \ {j}]
CountMsgs[P \in SUBSET Peer] == IF P = {} THEN 0
                                      ELSE LET i == CHOOSE p \in P: TRUE 
                                           IN Count[i, Peer] + 
                                              CountMsgs[P \ {i}]
Liveness == msgCounter = MAX_MSG ~> /\ \A p1 \in Peer, p2 \in Peer: Len(commChannels[p1, p2].in) = 0
                                /\ CountMsgs[Peer] = MAX_MSG  
============================================================

The model:

Declared constants:

IHave <- "IHave"
Peer <- {1,2,3}
MBody <- [model value] {b1,b2,b3}
Nil <- 0
Msg <- ProtoMsg
Prune <- "Prune"
Graft <- "Graft"
MAX_MSG <- 2
PeerSamplingService <- (1 :> {2,3} @@ 2 :> {1,3} @@ 3 :> {1,2})
Gossip <- "Gossip"

Initial predicate and next-state relation:

Init: InitPT
Next: NextPT

checking invariant TypeOk and property ReachConsistency

file attachments

Closed Oct 7, 2016 at 4:45 PM by mku
Closed as per last comment

comments

mku wrote Dec 21, 2015 at 1:18 PM

Hi,

if you turn off the property "ReachConsistency" TLC finds other less bizarre problems in your spec (i.e. commChannels is changed when declared UNCHANGED...). Please fix those first.

Thanks

niraamit wrote Dec 21, 2015 at 1:37 PM

With the latest upload of plumtree.tla I don't get errors other than a deadlock, which is fine by me because i want an error trace of states to explore. Is this ok?

niraamit wrote Dec 21, 2015 at 1:54 PM

Oh, now I can't reproduce it... I thought it was still happening but it doesn't :-/
So never mind, I will submit another issue if I have a proper spec causing it.
Thanks.