spin: modex_model3.pml.nvr:5, Error: syntax error, saw ''/' = 47'

Question

everyone! when I run the following pml file with spin command:

pml file: [https://github.com/kikishao/ACC/blob/main/modex_model3.pml]

spin command:

spin -f !([] (((((states==stop)&&(currentspeed==0)&&(timeGap==0)))-((controlAction==fullystop))))) -a -lm modex_model3.pml

I get the error message:

spin: modex_model3.pml.nvr:5, Error: syntax error       saw ''/' = 47'
spin: modex_model3.pml.nvr:5, Error: syntax error       saw ''/' = 47'
spin: modex_model3.pml.nvr:11, Error: aborting (ana_stmnt)

Firstly, I don't know how to view modex_model3.pml.nvr files, and secondly, what does "/" mean?how can i fix it? thanks!!!

Answer 1

1. You have a space in your argument, so the entire thing needs to be enclosed in quotes.

2. You are using - in your LTL formula, which isn't valid LTL according to SPIN. Maybe you meant to use -> for an implication?