Spinroot

Maxvonhippel

Member

Registered: 2019-09-13

Posts: 20

Trigraphs - what are they, how to use them?

In a model of mine, I have the following code:

chan daisy_memory_bit_1 = [10] of { bit }
bit tmp_bit_1;
daisy_memory_bit_1??<tmp_bit_1>;

and similar code for some other variables and channels.  Now, when I run my model I get this error message:

(base) max@max-XPS-13-9310:~/projects/research/nds2/KORG/korg-update$ spin -run -a -DNOREDUCE SCTP.attack2.pml_daisy_check.pml
SCTP.attack2.pml_daisy_check.pml:408:30: warning: trigraph ??< ignored, use -trigraphs to enable [-Wtrigraphs]
  408 |  :: daisy_memory_mtype_msgs_0??<tmp_mtype_msgs_0>;
      |                               
SCTP.attack2.pml_daisy_check.pml:409:23: warning: trigraph ??< ignored, use -trigraphs to enable [-Wtrigraphs]
  409 |     daisy_memory_bit_1??<tmp_bit_1>;
      |                       
SCTP.attack2.pml_daisy_check.pml:410:23: warning: trigraph ??< ignored, use -trigraphs to enable [-Wtrigraphs]
  410 |     daisy_memory_bit_2??<tmp_bit_2>;
      |                       
ltl newPhi: (! (<> ((b==1)))) || ([] (! (witnessAttack2)))
In file included from pan.c:12693:
pan.t: In function ‘settable’:
pan.t:168:64: warning: trigraph ??< ignored, use -trigraphs to enable [-Wtrigraphs]
  168 |  trans[3][49] = settr(774,0,50,39,39,"daisy_memory_mtype_msgs_0??<tmp_mtype_msgs_0>", 1, 519, 0);
      |                                                                 
pan.t:169:57: warning: trigraph ??< ignored, use -trigraphs to enable [-Wtrigraphs]
  169 |  trans[3][50] = settr(775,0,51,40,40,"daisy_memory_bit_1??<tmp_bit_1>", 1, 518, 0);
      |                                                         
pan.t:170:57: warning: trigraph ??< ignored, use -trigraphs to enable [-Wtrigraphs]
  170 |  trans[3][51] = settr(776,0,55,41,41,"daisy_memory_bit_2??<tmp_bit_2>", 1, 517, 0);
      |   

When I tried running again with options -trigraphs or -Wtrigraphs, it did not change.  How can I address this?

What I am trying to accomplish is non-deterministically read from the channel to the temporary variable, without removing the message being read from the channel.

Thanks!

Kai

Member

Registered: 2011-08-17

Posts: 6

Re: Trigraphs - what are they, how to use them?

`-trigraph` is a gcc option to interpret 3-character sequences such s `??<` as something else. It has nothing to do with spin. I'd add spaces around the `??` to avoid this issue.

Either way, none of this will help you to

> non-deterministically read

because you will always receive the first matching message from the channel, at least according to the spin manpage on receive.