mbeddr / mbeddr.formal

FASTEN: FormAl SpecificaTion ENvironment - a set of DSLs to experiment with rigorous systems and safety engineering.
https://sites.google.com/site/fastenroot/home
Apache License 2.0
23 stars 14 forks source link

Signed and unsigned word not permitted as type #61

Closed robertguetzkow closed 3 years ago

robertguetzkow commented 3 years ago

I was trying to extend the _010_traffic_lights_controller_baseLang example with additional variables and noticed that FASTEN doesn't seem to accept variables of type unsigned word [N] and signed word [N]. Is this a user error or does FASTEN limit the allowed types for state machines?

  VAR {                                                                       
    state variable traffic : {Green, Yellow, Red};                            
    pedestrian : {Walk, DontWalk};                                            
    timer : 0..10;                                                            
    abc : signed word [5];                                                    
  }

Error message on hover: Abstract concept instance detected. Use one of sub-concepts instead. Concept: Type

Apologies if this is a trivial mistake caused by my inexperience with FASTEN and NuSMV.

danielratiu commented 3 years ago

If you type "word" and start auto-completion (ctrl+space) then FASTEN creates an "unsigned word"

image

Please confirm that it works like this.

If you want to change the signedness (i.e. to "signed") there is an intention (alt + enter) - unfortunately it seems that there is an MPS bug which prevents correct functioning of this intention. I have commited a fix on FASTEN side to avoid the MPS issue https://youtrack.jetbrains.com/issue/MPS-33284

Workaround for changing the signedness - right click on the type, select "show reflective editor" and change the "signed" flag.

robertguetzkow commented 3 years ago

Thank you for the quick reply. That seems to do the trick.