search

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

Attributes in Assemblies #12

Closed markusvoelter closed 4 years ago

markusvoelter commented 5 years ago

Our components have internal state, for example, a failure_count. This is used in contracts. RIght now it looks as if it is not possible to have properties/variables/attributes in assemblies. Is this planned?

danielratiu commented 5 years ago

Currently we support annotating SMV modules with contracts. In those contracts one can reference internal variables defined in modules. Would this be enough for your use-cases?

danielratiu commented 4 years ago

talked to Markus and it is OK for now