A forum for Spin users
You are not logged in.
Pages: 1
It turns out to be a problem with evince on my machine, it doesn't show the full page. I used gv to view the file in its full feature with the options of unselecting "state > respect document structure". Thanks again.
mtype {P,G,V};
chan ch = [0] of {mtype};
active proctype foo(){
a:
ch?P;
ch!G;
ch?V;
goto a
}
active proctype bar(){
b:
ch!P;
ch?G;
ch!V;
goto b
}
Try spin -u25 -M foo.pml
Sorry to disturb. This minimum example finally compiled and it spent some time to generate the automata (with 3122 lines, 170082 characters).
Thanks root. I was replaying .trail. I used
spin -M -t foo.pml
It was in two pages, but some part (considerably a lot) is missing between page 1 and page 2.
The minimum way to reproduce this case:
init{
skip
}
#define fair_run (([]<> (_last == 3)) && ([]<> (_last == 4)) && ([]<> (_last == 5)) && ([]<> (_last == 6)))
ltl fr {!fair_run }
Is my ltl specified in a wrong way?
The right pane paralleling the code under Simulate/Replay tab shows the channel messages flow, but I would like to checked it outside iSpin, as the chart is much bigger than the pane. Also, this pane can only be scrolled by the bars (instead the code pane we can use touchpad). I tried to resize the pane by the square box, but it is not yet ideal. The "Save" button at the right-top corner only saves the part shown.
Pages: 1