The syntax of PROMELA

jllang · 2021-08-21 19:57:32

It seems that there are some differences between the documented syntax of PROMELA and the syntax accepted by Spin. I made some findings while developing my own parser for PROMELA. I wrote my own EBNF for the dialect accepted by my tool along with some comments on the PROMELA syntax. I'd appreciate comments very much. My EBNF is available at GitHub: https://gist.github.com/jllang/54ff523beafa82058d05dd829ccc2671

jllang · 2021-09-03 10:36:10

Is the sublanguage that can occur in traces documented?

spinroot · 2022-03-01 19:12:16

not sure what you mean by "the sublanguage that can occur in traces"
you mean the format and syntax of error traces?

jllang · 2022-03-04 17:38:06

I mean the statements that can occur in transitions in a trace.

spinroot · 2022-03-04 18:02:51

they should be basic statements from the model
so it's mostly Promela syntax -- d_steps are special though
since they are converted into a single transition

jllang · 2022-03-05 16:01:28

I've also encountered lines containing `DO`, `IF`, and `.(goto)` as the statement. I presume `DO` and `IF` mean that the process is choosing between possible branches in a `do` or `if` statement. Is `.(goto)` a goto statement that was generated from a `for` loop?

Last edited by jllang (2022-03-05 16:01:50)

spinroot · 2022-03-05 19:24:30

the .(goto) links are generated by the parser. e.g. to encode break statements etc

jllang · 2022-03-12 10:35:18

Okay, thanks.

Spinroot

#1 2021-08-21 19:57:32

The syntax of PROMELA

#2 2021-09-03 10:36:10

Re: The syntax of PROMELA

#3 2022-03-01 19:12:16

Re: The syntax of PROMELA

#4 2022-03-04 17:38:06

Re: The syntax of PROMELA

#5 2022-03-04 18:02:51

Re: The syntax of PROMELA

#6 2022-03-05 16:01:28

Re: The syntax of PROMELA

#7 2022-03-05 19:24:30

Re: The syntax of PROMELA

#8 2022-03-12 10:35:18

Re: The syntax of PROMELA

Board footer