Spinroot

A forum for Spin users

You are not logged in.

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

jllang
Member
From: Finland
Registered: 2021-05-05
Posts: 27

The syntax of PROMELA

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

Offline

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

jllang
Member
From: Finland
Registered: 2021-05-05
Posts: 27

Re: The syntax of PROMELA

Is the sublanguage that can occur in traces documented?

Offline

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

spinroot
forum
Registered: 2010-11-18
Posts: 694
Website

Re: The syntax of PROMELA

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

Offline

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

jllang
Member
From: Finland
Registered: 2021-05-05
Posts: 27

Re: The syntax of PROMELA

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

Offline

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

spinroot
forum
Registered: 2010-11-18
Posts: 694
Website

Re: The syntax of PROMELA

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

Offline

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

jllang
Member
From: Finland
Registered: 2021-05-05
Posts: 27

Re: The syntax of PROMELA

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)

Offline

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

spinroot
forum
Registered: 2010-11-18
Posts: 694
Website

Re: The syntax of PROMELA

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

Offline

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

jllang
Member
From: Finland
Registered: 2021-05-05
Posts: 27

Re: The syntax of PROMELA

Okay, thanks.

Offline

Board footer

Powered by FluxBB