[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Evaluating an expression of the form t \o s when s is not a string: <<>>



Hello,

On 12 Aug 2022, at 04:01, Anand Kumar <akkeshavan@xxxxxxxxx> wrote:

SendMessage  is defined as follows:

SendMessage( blockId, channel) ==

    Append(channel, blockId)

OK, but it is used as

   SendMessage(Channel,Blocks[self].outputs[index])

Aren't the two parameters reversed?

Stephan




Here is the full spec:

EXTENDS Integers, Sequences, TLC


 


CONSTANTS  MaxChannelSize 

 


RemoveMessagesForBlock(block, channel) ==

  [j \in 1..(Len(channel)-1) |-> IF block.id = channel[j] THEN channel[j+1] 

                                      ELSE channel[j]]

 

BlockHasMessages(block, channel) ==

        \E message \in channel : block.id = message

SendMessage( blockId, channel) ==

    Append(channel, blockId)

 

(*--algorithm flow

variables 

    StateSet = { "waiting", "processing", "end"};


    Blocks =  [

      a |->  [ id |-> "a", state |-> "waiting", inputs |->0, outputs|-> <<"b","c">>],

      b |->   [ id |-> "b", state |-> "waiting", inputs |->1, outputs|-> <<"c","d">>],

      c |->  [ id |-> "c", state |-> "waiting", inputs |->2, outputs|-> <<"d">>],

      d |->   [ id |-> "d", state |-> "waiting", inputs |->2, outputs|-> <<>>]

    

    ];

    

    Channel = <<>>;

     
    

define

   BoundedQueue == Len(Channel) <= MaxChannelSize

   TypeOK == 

        \A block \in Blocks:  block.state \in StateSet

   EventuallyTerminates ==

       <>[] \A block \in Blocks: block.state = "end"

   

end define;


 




 


process blockDefs \in {"a", "b", "c", "d"}

    variables

        index =1;

begin execute:

    

    while Blocks[self].state /= "end" do


        if Blocks[self].state = "waiting" /\ Blocks[self].inputs = 0 then

            Blocks[self].state := "processing";

        elsif Blocks[self].state ="waiting" /\ Blocks[self].inputs >0 then

            waitInput:

              

                if BlockHasMessages(Blocks[self],Channel) then

                    Channel := RemoveMessagesForBlock(Blocks[self],Channel);

                    Blocks[self].state := "processing";

                else

                    skip;

                end if;

        elsif Blocks[self].state = "processing" then

            writeOutputs:

                while index < Len(Blocks[self].outputs) do

                    Channel := SendMessage(Channel,Blocks[self].outputs[index]);

                    index := index+1;

                end while;

            end_state:

                Blocks[self].state := "end";

        else       

            skip;

        end if;

    end while;

    

end process;

 


end algorithm; *)

\* BEGIN TRANSLATION (chksum(pcal) = "24e11c4a" /\ chksum(tla) = "22972279")

VARIABLES StateSet, Blocks, Channel, pc


(* define statement *)

BoundedQueue == Len(Channel) <= MaxChannelSize

TypeOK ==

     \A block \in Blocks:  block.state \in StateSet

EventuallyTerminates ==

    <>[] \A block \in Blocks: block.state = "end"


VARIABLE index


vars == << StateSet, Blocks, Channel, pc, index >>


ProcSet == ({"a", "b", "c", "d"})


Init == (* Global variables *)

        /\ StateSet = { "waiting", "processing", "end"}

        /\ Blocks =           [

                      a |->  [ id |-> "a", state |-> "waiting", inputs |->0, outputs|-> <<"b","c">>],

                      b |->   [ id |-> "b", state |-> "waiting", inputs |->1, outputs|-> <<"c","d">>],

                      c |->  [ id |-> "c", state |-> "waiting", inputs |->2, outputs|-> <<"d">>],

                      d |->   [ id |-> "d", state |-> "waiting", inputs |->2, outputs|-> <<>>]

                    

                    ]

        /\ Channel = <<>>

        (* Process blockDefs *)

        /\ index = [self \in {"a", "b", "c", "d"} |-> 1]

        /\ pc = [self \in ProcSet |-> "execute"]


execute(self) == /\ pc[self] = "execute"

                 /\ IF Blocks[self].state /= "end"

                       THEN /\ IF Blocks[self].state = "waiting" /\ Blocks[self].inputs = 0

                                  THEN /\ Blocks' = [Blocks EXCEPT ![self].state = "processing"]

                                       /\ pc' = [pc EXCEPT ![self] = "execute"]

                                  ELSE /\ IF Blocks[self].state ="waiting" /\ Blocks[self].inputs >0

                                             THEN /\ pc' = [pc EXCEPT ![self] = "waitInput"]

                                             ELSE /\ IF Blocks[self].state = "processing"

                                                        THEN /\ pc' = [pc EXCEPT ![self] = "writeOutputs"]

                                                        ELSE /\ TRUE

                                                             /\ pc' = [pc EXCEPT ![self] = "execute"]

                                       /\ UNCHANGED Blocks

                       ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]

                            /\ UNCHANGED Blocks

                 /\ UNCHANGED << StateSet, Channel, index >>


waitInput(self) == /\ pc[self] = "waitInput"

                   /\ IF BlockHasMessages(Blocks[self],Channel)

                         THEN /\ Channel' = RemoveMessagesForBlock(Blocks[self],Channel)

                              /\ Blocks' = [Blocks EXCEPT ![self].state = "processing"]

                         ELSE /\ TRUE

                              /\ UNCHANGED << Blocks, Channel >>

                   /\ pc' = [pc EXCEPT ![self] = "execute"]

                   /\ UNCHANGED << StateSet, index >>


writeOutputs(self) == /\ pc[self] = "writeOutputs"

                      /\ IF index[self] < Len(Blocks[self].outputs)

                            THEN /\ Channel' = SendMessage(Channel,Blocks[self].outputs[index[self]])

                                 /\ index' = [index EXCEPT ![self] = index[self]+1]

                                 /\ pc' = [pc EXCEPT ![self] = "writeOutputs"]

                            ELSE /\ pc' = [pc EXCEPT ![self] = "end_state"]

                                 /\ UNCHANGED << Channel, index >>

                      /\ UNCHANGED << StateSet, Blocks >>


end_state(self) == /\ pc[self] = "end_state"

                   /\ Blocks' = [Blocks EXCEPT ![self].state = "end"]

                   /\ pc' = [pc EXCEPT ![self] = "execute"]

                   /\ UNCHANGED << StateSet, Channel, index >>


blockDefs(self) == execute(self) \/ waitInput(self) \/ writeOutputs(self)

                      \/ end_state(self)


(* Allow infinite stuttering to prevent deadlock on termination. *)

Terminating == /\ \A self \in ProcSet: pc[self] = "Done"

               /\ UNCHANGED vars


Next == (\E self \in {"a", "b", "c", "d"}: blockDefs(self))

           \/ Terminating


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


Termination == <>(\A self \in ProcSet: pc[self] = "Done")


\* END TRANSLATION 


On Thursday, 11 August 2022 at 17:45:53 UTC+5:30 Stephan Merz wrote:
Since you do not show your full spec, I can only make a guess on what is going on here. It looks like Channel is a sequence, and you are trying to send some data item on that channel. In that case, SendMessage(ch, d) should be defined as Append(ch, d), not as ch \o d, since \o represents sequence concatenation.

Stephan

On 11 Aug 2022, at 12:31, Anand Kumar <akkes...@xxxxxxxxx> wrote:

TLC generates this error>

There is also a warning that "writeOutputs"  is never enabled


elsif Blocks[self].state = "processing" then

            writeOutputs:

                while index < Len(Blocks[self].outputs) do

                    Channel := SendMessage(Channel,Blocks[self].outputs[index]);

                    index := index+1;

                end while;


>>> generated TLA code

writeOutputs(self) == /\ pc[self] = "writeOutputs"

                      /\ IF index[self] < Len(Blocks[self].outputs)

                            THEN /\ Channel' = SendMessage(Channel,Blocks[self].outputs[index[self]])

                                 /\ index' = [index EXCEPT ![self] = index[self]+1]

                                 /\ pc' = [pc EXCEPT ![self] = "writeOutputs"]

                            ELSE /\ pc' = [pc EXCEPT ![self] = "end_state"]

                                 /\ UNCHANGED << Channel, index >>


                      /\ UNCHANGED << StateSet, Blocks >>



--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d5459d87-f821-4f36-929c-e09a302436b7n%40googlegroups.com.


--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/710147f8-1d58-40da-98ac-308137b61685n%40googlegroups.com.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/BE9FD328-05F6-4764-9B19-64D9AD801167%40gmail.com.