Project

General

Profile

Actions

Feature #10940

closed

Always specify specifications set in job.json

Added by Evgeny Novikov about 3 years ago. Updated almost 3 years ago.

Status:
Closed
Priority:
High
Category:
-
Target version:
Start date:
09/16/2021
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

At the moment EMG has some quite tricky rules to select necessary environment model specifications, so that users may be completely unaware about a set of specifications used. I suggest to at least explicitly specify "specifications set" in all job.json and fail early when this is not the case or maybe when the user provides something unsupported (there may be a static list of supported specification sets in job.py). Moreover, rather than using implicit inheritance rules (as far as I understand some environment model specifications are marked as "referenced" and they are used for those specification sets for which they are not provided explicitly), I suggest to explicitly map subsets of specification sets to appropriate specifications. For instance, instead of using something like this:

{
    "3.14" : {... "reference": true ...},
    "5.5": {...}
}

you can use something like you use for function models:
{
    "3.14, 4.17" : {...},
    "5.5": {...}
}

BTW, I do believe that spending much effort for development of specifications is strictly necessary for using software model checkers, so it's pretty well to "waste" several minutes to explicitly map specification sets to specifications when adding support for a new specification set.


Related issues 2 (1 open1 closed)

Related to Klever - Feature #11106: Define default environment model specificationsNew12/10/2021

Actions
Blocks Klever - Feature #10932: Output intermediate environment models in a more user-friendly wayClosedEvgeny Novikov09/09/2021

Actions
Actions

Also available in: Atom PDF