A forum for Spin users
You are not logged in.
Pages: 1
Hi! I'm new on SpinRoot.
When I try to check my Promela Code, Spin returns:
Error: syntax error saw ''(' = 40'
Error: syntax error saw ''(' = 40'
Error: syntax error saw 'process name' near 'set_syntax'
Error: syntax error saw 'an identifier' near 'X_obj'
Error: no runable process
40 there isn't a symbol in my code, someone can help me? Thanks in advance.
-
sylvy
Offline
Yes sure.
spin: promela_c.pml:61, Error: syntax error saw ''(' = 40'
59 proctype Copy_Init()
60 {
61 set_syntax(variable, -1, 1);
62 set_syntax(variable, -1, 3);
63 set_syntax(variable, -1, 4);
64 set_syntax(variable, -1, 5);
65 set_syntax(variable, -1, 8);
66 set_syntax(variable, -1, 10);
67 set_syntax(variable, -1, 14);
68 }
spin: promela_c.pml:160, Error: syntax error saw ''(' = 40'
spin: promela_c.pml:160, Error: syntax error saw 'process name' near 'set_syntax'
spin: promela_c.pml:160, Error: syntax error saw 'an identifier' near 'X_obj'
158 s1:
159 if
160 ::flow[c_copy]?inn -> Copy_Init();Copy_Copy();Copy_getFileUtils();Copy_setToFile();Copy_setToDir();Copy_setToDir();Copy_createFilterSet();Copy_setPreserveLastModified();Copy_setVerbose();Copy_execute();Copy_getFilterSet();flow[c_run]!out;
161 goto s0;
162 fi;
Offline
by the way, 40 is just the decimal value of the character '('
it is the ( that is in an unexpected place in the input
the error is flagged on line 160 which contains "Copy_Init();" as if it was a function call.
but it actually is a proctype name, so the invocation should be "run Copy_Init();"
note though that this does not behave like a function call in other ways: it
simply starts an additional asynchronous process that will run separately from the process
that executes the run command on line 160, and in parallel with it
Offline
there are indeed no active processes
you will need to have at least one process running at the start
that can create the other processes
normally that would be a process cannled 'init' but you can pick
any other process (maybe your process copy_java?) and prefix the proctype
declaration with the keyword 'active' : active proctype copy_java() { .... }
but it does look like you are trying to use processes as functions, and that
can very easily produce the wrong result
note for instance that if you say:
run A();
run B();
then B() may actually finish executing all its statements before A() even starts.
The reason is that 'run' merely starts a new thread of execution that runs in
parallel with all others -- after the statement 'run A();' completes then there
is simply one extra process competing for execution -- it may or may not run
for a while.
You probably want to use 'inline's for some of the proctypes, for instance
inline set_syntax(count, next)
an inline is line a macro (but looks nicer), and executes right away
other than that, I see that your copy_java() process receives messages,
but there are no processes anywhere that can send those messages.
a Spin model must be "closed" i.e., you have to specify all input sources
within the model -- or else you cannot exhaustively verify its behavior
Offline
Wow...That good. Thanks for sharing.
Offline
The same error you receive if you call a function with a name other then the one you defined,so check before testing with spin.
Offline
Pages: 1