A forum for Spin users
You are not logged in.
Pages: 1
works fine now, many thanks!
Just the version-string in the ispin script is still set to "1.1.0" which was a little confusing at first.
Indeed, there seems to be a difference in the format of dot-files produced by actual dot-versions (2.29 and higher) compared to older versions:
* there are additional linebreaks in statements (not critical I guess), and
* there is no ordering of statements any more, i.e. there used to be all nodes first, then all edges listed in the dot file.
The grammar for the dot language does not specify a certain ordering. However, older versions of dot seemed to produce this ordering in their output files. If any parser implicitely relies on a certain ordering of the dot-statements, then it now may fail.
I did not look very deep in the spin script, but I interpret the error "invalid bareword e" while parsing the dot file as follows:
Nodes and transition have an attribute "pos=..." with a numeric value for nodes, while the value for transitions starts with "e,...". So parsing a transition while expecting a node gives a symbol that makes no sense in numerical calculations.
Maybe this helps to make ispin work with the actual dot-versions.
A workaround could be to sort the dot file before parsing.
I used to have graphviz version 2.29 and just updated to:
dot - graphviz version 2.31.20130115.0545 (20130115.0545)
Would be interesting to see if you can reproduce the error with a version 2.29 or higher. For Ubuntu there is version 2.30 available.
Otherwise it's a specific problem of the macos-version. Older version-numbers for mountain lion are not available.
I will also try to find out if the format has changed and compare it with an example file from a different machine.
Hello,
I am using spin 6.2.3, ispin 1.1.0 with tcl/tk 8.5/8.5 on mac os 10.8.2. Before displaying the automata view of the init process of the standard example ex_1a.pml (after clicking on ""init") I get the following tcl/tk-script error:
invalid bareword "e"
in expression "50 * e=";
should be "$e" or "{e}" or "e(...)" or ...
invalid bareword "e"
in expression "50 * e=";
should be "$e" or "{e}" or "e(...)" or ...
(parsing expression "50 * e=")
invoked from within
"expr 50 * $mf"
(procedure "find_field" line 10)
invoked from within
"find_field "width=" $line"
(procedure "display_graph" line 129)
invoked from within
"display_graph init"
(command bound to event)
The automata view is very useful in teaching, I appreciate any suggestions.
Many thanks,
Heinz
Here is some more information that might help:
When looking at the reachable states in the system automaton after verification (using spin spider) there is only one endstate present, namely the one with n==1. There is a transition in the diagram from state (P:end, Q: n=2, n==1 ) to state (P:end, Q:end, n==1), so setting n=2 is not recognized.
I checked that this was also true in spin version 4.3.0.
Hello,
I just observed that enabling/disabling weak fairness (wf) affects the outcome of verifying "<>[](n==1)" in the following simple model:
byte n = 0;
active proctype P() { n=1 }
active proctype Q() { n=2 }
Clearly, there should be two endstates with n==1 and n==2, respectively. Spin reports an error for the above ltl-formula only if wf is turned off, which I find surprising because I don't think that there are unfair computation paths. The same behaviour appears when "1" is replaced by "0" or "2" in the formula. For values n==3,4,... there is always an error reported by spin independently from wf.
A similar behaviour can be observed with "<>[](n==0)" and the following model:
byte n = 0;
active proctype P() {
if
:: n=1
:: n=2
fi
}
So my question is why does enabling/disabling weak fairness have an effect on these verifications?
Many thanks in advance,
Heinz
Pages: 1