CODEWITHSUNDEEP
formal-verification
DeadlyKitten999
DeadlyKitten999

Reputation: 67

problem with comparing the pseudocode with lustre

I have a problem related with lustre. I have this pseudocode :

Process x(in int a, in int b, out int x){
   int k; bool sw=true;
   loop forever
      if sw then
         k = a.receive();
      else
         k = b.receive();
      end if;
   x.send(k);
   sw = !sw;
end loop;
}

I did the lustre code like this :

node process_p3 (a,b:int) returns (x:int);
var k: int;
var sw: bool;
let
    sw = true -> not pre(sw); --loop forever?
    k=if sw then a else b;
    x=k;
tel

my question here is, does this lustre code correctly describe the pseudocode? I just feel some doubt regarding the sw state in "loop forever" condition..In my opinion, the sw in pseudocode stays false forever after the first state (which is true)...an I am not really sure if the lustre code really represents the pseudocode written above..any response is really appreciated, thx before.

Upvotes: 0

Views: 15

Answers (0)

Related Questions