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

[WiP] Initial OCRA language integration #47

Closed jensbuehl closed 3 years ago

jensbuehl commented 4 years ago

As discussed, the initial OCRA language integration which was moved from proprietary BOSCH repository.

danielratiu commented 4 years ago

Hi Jens,

thank you for the pull-request!

I pushed in the repo a new branch called "feature/ocra" containing your code + a commit in which I moved the ocra language into the proper directory. In addition, I have also did some clean-up commits - please have a look to double-check that I did not delete/changed things in a bad manner.

Also, could you check that all non-abstract concepts are instantiated at least in one example from the sandbox solution?

I remarked that some operators have been re-implemented (instead of being reused from the 'com.mbeddr.formal.base.expressions' language) - e.g. relational operators. This will lead to confusions - e.g. in the following node, less-equals comes once from the ocra language and once from the mbeddr.formal.base.expressions language project: com.mbeddr.formal.nusmv (C:\work\mbeddr.formal\code\languages\com.mbeddr.formal.nusmv) module: com.mbeddr.formal.ocra.sandbox model: com.mbeddr.formal.ocra.sandbox root: ComplexExample [OthelloSystemSpecification] node: null [Guarantee] url: http://127.0.0.1:63320/node?ref=r%3A098b9963-beaa-42d7-9080-d0509664a285%28com.mbeddr.formal.ocra.sandbox%29%2F6677499667399352630

Could we re-use only the existing operators and not re-implement them?

The textgens are missing - could you please add them?

Also, a minimal functionality to start OCRA on the generated files and present the results would be really useful (also only as raw text if the lifting is too complex). As of now, the integration of OCRA is restricted only to creating models.

A few unit tests for running OCRA on generated files to make sure that we do not get regressions in future.

Dan

norro commented 4 years ago

@danielratiu I suggest we make a first merge of this pull request once the textgen is included (probably within this week) and redundant expressions are sorted out. Then after migration to MPS 2020.2 we do the integration with the actual OCRA tool in a separate PR. Does this sound good to you?

danielratiu commented 4 years ago

@norro your plan seems fine to me

jensbuehl commented 3 years ago

@danielratiu As discussed, I just rebased on mbeddr/master

norro commented 3 years ago

There seem to be two versions of the language, see https://github.com/jenzb/mbeddr.formal/tree/ocra/code/languages/com.mbeddr.formal.ocra and https://github.com/jenzb/mbeddr.formal/tree/ocra/code/languages/com.mbeddr.formal.nusmv/languages/com.mbeddr.formal.ocra

norro commented 3 years ago

@danielratiu @jenzb is there still anything blocking this PR from being merged?

jensbuehl commented 3 years ago

Aus meiner Sicht nicht. Die "offenen Punkte" habe ich dir ja letztes Jahr zukommen lassen.

Von: Arne Nordmann notifications@github.com Gesendet: Donnerstag, 21. Januar 2021 16:43 An: mbeddr/mbeddr.formal mbeddr.formal@noreply.github.com Cc: Jens jens.buehl@outlook.com; Mention mention@noreply.github.com Betreff: Re: [mbeddr/mbeddr.formal] [WiP] Initial OCRA language integration (#47)

@danielratiuhttps://github.com/danielratiu @jenzbhttps://github.com/jenzb is there still anything blocking this PR from being merged?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHubhttps://github.com/mbeddr/mbeddr.formal/pull/47#issuecomment-764732695, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AA6MUKNFJ6CXTATKJ3NMV6LS3BDSRANCNFSM4R5ZXA4A.

ratiud commented 3 years ago

I have looked over the current branch and there are two points we should address before merging:

1) the OCRA language does not have a textgen - the sandbox models cannot be generated ... do you plan to implement this? (to have a minimal working example of being able to create a model and generate OCRA code - via textgen)

2) the pluginSolution contains only empty code - please either a) implement a minimal functionality to run OCRA on the generated code and display the result in "Raw results view", or b) delete the pluginSolution (it is empty now anyway ...)

norro commented 3 years ago

Superseded by https://github.com/mbeddr/mbeddr.formal/pull/57, including textgen