Skip to content
This repository was archived by the owner on May 18, 2019. It is now read-only.

Commit fdfc424

Browse files
Lena BuffoniOpenModelica-Hudson
Lena Buffoni
authored and
OpenModelica-Hudson
committed
support for verification scenario generation from requirement models
1 parent f727803 commit fdfc424

File tree

3 files changed

+165
-47
lines changed

3 files changed

+165
-47
lines changed

‎Compiler/FrontEnd/ModelicaBuiltin.mo‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2198,6 +2198,13 @@ external "builtin";
21982198
annotation(preferredView="text");
21992199
end inferBindings;
22002200

2201+
function generateVerificationScenarios
2202+
input TypeName path;
2203+
output Boolean success;
2204+
external "builtin";
2205+
annotation(preferredView="text");
2206+
end generateVerificationScenarios;
2207+
22012208
public function rewriteBlockCall "Function for property modeling, transforms block calls into instantiations for a loaded model"
22022209
input TypeName className;
22032210
input TypeName inDefs;

‎Compiler/Script/Binding.mo‎

Lines changed: 145 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -86,73 +86,167 @@ algorithm
8686
out_model_def := Interactive.updateProgram(Absyn.PROGRAM({out_vmodel}, Interactive.buildWithin(model_path)), env);
8787
end inferBindings;
8888

89-
/*public function generateVerificationScenarios "@autor lenab : root function called from API "
89+
public function generateVerificationScenarios "@autor lenab : root function called from API "
9090
input Path package_path "The package where the bindings will be generated";
9191
input Absyn.Program in_env "All loaded models";
9292
output Absyn.Program out_env;
9393

9494
protected
9595
list<Mediator> ms;
96-
Absyn.Class package_def, out_vmodel;
96+
Absyn.Class package_def, out_vmodel, autogen_class, autogen_class2;
9797
list<SCode.Element> scode_def;
98+
List<tuple<SCode.Element, String>> design_alts, reqs, scenarios;
9899
list<Client_e> client_list;
100+
list<Absyn.ElementItem> ag_elems, autogen_model_list;
101+
Absyn.ElementItem autogen_model;
102+
Integer i;
99103
algorithm
104+
scode_def := SCodeUtil.translateAbsyn2SCode(in_env);
100105
// get all design alternatives
106+
design_alts := getAllElementsOfType(scode_def, "Design", "", {});
101107
// get all requirements
108+
reqs := getAllElementsOfType(scode_def, "Requirement", "", {});
102109
// get all scenarios
110+
scenarios := getAllElementsOfType(scode_def, "Scenario", "", {});
111+
// get mediators
103112
ms := getMediatorDefsElements(scode_def, {});
113+
104114
package_def := Interactive.getPathedClassInProgram(package_path, in_env);
105-
out_env := in_env;
106-
end generateVerificationScenarios; */
115+
autogen_model_list := {};
116+
i:=0;
117+
for d in design_alts loop
118+
for s in scenarios loop
119+
ag_elems := populateModel(d::s::reqs, 0 , {});
120+
121+
autogen_class := Absyn.CLASS("verif_model_autogen_" + intString(i),
122+
false, false, false, Absyn.R_MODEL(),
123+
Absyn.PARTS({}, {}, {Absyn.PUBLIC(ag_elems)},{},
124+
SOME("Autogenerated verification model")), Absyn.dummyInfo);
125+
client_list := buildInstList(autogen_class, in_env, NO_PRED(), ms, {});
126+
autogen_class2 := inferBindingClientList(client_list, autogen_class, in_env);
127+
print(Dump.unparseClassStr(autogen_class2) + "\n");
128+
129+
autogen_model := Absyn.ELEMENTITEM(Absyn.ELEMENT(false, NONE(), Absyn.NOT_INNER_OUTER(),
130+
Absyn.CLASSDEF(false, autogen_class2), Absyn.dummyInfo, NONE()));
131+
autogen_model_list := autogen_model::autogen_model_list;
132+
i:= i+1;
133+
end for;
134+
end for;
135+
out_vmodel := updatePackage(package_def, autogen_model_list);
136+
//print(Dump.unparseClassStr(out_vmodel) + "\n");
137+
out_env := Interactive.updateProgram(Absyn.PROGRAM({out_vmodel}, Interactive.buildWithin(package_path)), in_env);
138+
end generateVerificationScenarios;
139+
140+
public function updatePackage
141+
input Absyn.Class in_class;
142+
input list<Absyn.ElementItem> ag_elems;
143+
output Absyn.Class out_class;
144+
algorithm
145+
out_class := match(in_class)
146+
local
147+
list<Absyn.Class> r_classes, nr_classes;
148+
Absyn.Class cls, n_cls;
149+
Absyn.Ident name;
150+
Boolean partialPrefix, finalPrefix, encapsulatedPrefix;
151+
Absyn.Restriction restriction;
152+
Absyn.ClassDef body, nbody;
153+
SourceInfo info ;
154+
list<String> typeVars ;
155+
list<Absyn.NamedArg> classAttrs ;
156+
list<Absyn.ClassPart> classParts, nclsp;
157+
list<Absyn.Annotation> ann ;
158+
Option<String> comment;
159+
case(Absyn.CLASS(name, partialPrefix, finalPrefix, encapsulatedPrefix, restriction, Absyn.PARTS(typeVars, classAttrs, classParts, ann, comment), info))
160+
equation
161+
nbody = Absyn.PARTS(typeVars, classAttrs, {Absyn.PUBLIC(ag_elems)}, ann, comment);
162+
then
163+
Absyn.CLASS(name, partialPrefix, finalPrefix, encapsulatedPrefix, restriction, nbody, info);
164+
end match;
165+
end updatePackage;
166+
167+
protected function populateModel
168+
input List<tuple<SCode.Element, String>> element_defs;
169+
input Integer autoVal;
170+
input List<Absyn.ElementItem> elements_in;
171+
output List<Absyn.ElementItem> elements_out;
172+
algorithm
173+
elements_out := match(element_defs)
174+
local
175+
list<SCode.Element> m;
176+
List<tuple<SCode.Element, String>> rest;
177+
Absyn.Element el;
178+
Absyn.Ident cname;
179+
String nName;
180+
String p_path;
181+
case {} then elements_in;
182+
case (SCode.CLASS(cname, _, _, _, _, _, _, _), p_path)::rest
183+
equation
184+
nName = if(p_path=="")then cname else p_path+"."+cname;
185+
el = Absyn.ELEMENT(false, NONE(), Absyn.NOT_INNER_OUTER(), Absyn.COMPONENTS(
186+
Absyn.ATTR(false, false, Absyn.NON_PARALLEL(), Absyn.VAR(), Absyn.BIDIR(), Absyn.NONFIELD(), {}),
187+
Absyn.TPATH(Absyn.stringPath(nName), NONE()), {Absyn.COMPONENTITEM(
188+
Absyn.COMPONENT("_agen_" + cname + intString(autoVal), {}, NONE()), NONE(), NONE())}), Absyn.dummyInfo, NONE());
189+
then populateModel(rest, autoVal+1, Absyn.ELEMENTITEM(el)::elements_in);
190+
end match;
191+
end populateModel;
192+
193+
107194

108195
protected function getAllElementsOfType
109196
input list<SCode.Element> element_defs;
110197
input Ident typeName;
111-
input List<SCode.Element> elements_in;
112-
output List<SCode.Element> elements_out;
198+
input String pathInProg;
199+
input List<tuple<SCode.Element, String>> elements_in;
200+
output List<tuple<SCode.Element, String>> elements_out;
113201
algorithm
114202
elements_out := match(element_defs)
115203
local
116-
list<SCode.Element> rest,m ;
204+
list<SCode.Element> rest;
205+
List<tuple<SCode.Element, String>> m;
117206
SCode.Element el;
118207
case {} then elements_in;
119208
case el::rest
120209
equation
121-
m = listAppend(getAllElementsOfType2(el, typeName), elements_in);
122-
then getAllElementsOfType(rest, typeName, m);
210+
m = listAppend(getAllElementsOfType2(el, typeName, pathInProg), elements_in);
211+
then getAllElementsOfType(rest, typeName, pathInProg, m);
123212
end match;
124213
end getAllElementsOfType;
125214

126215
protected function getAllElementsOfType2
127216
input SCode.Element el;
128217
input Ident typeName;
129-
output List<SCode.Element> res_elem;
218+
input String pathInProg;
219+
output List<tuple<SCode.Element, String>> res_elem;
130220
algorithm
131221
res_elem := matchcontinue(el)
132222
local
133223
Absyn.Ident n;
134224
list<SCode.Element> elist;
135225
SCode.Mod mod, clientMod, providerMod;
136226
list<Absyn.Exp> cMod, pMod, prMod;
137-
String template, mType, name, str1, str2;
227+
String template, mType, name, nName;
138228
Absyn.FunctionArgs pArgs, cArgs;
139229
list<Client> cls;
140230
list<Provider> prvs;
141231
list<Preferred> pref;
142-
case SCode.CLASS(_, _, _, _, SCode.R_PACKAGE(), SCode.PARTS(elist, _,_,_,_,_,_,_), _, _)
143-
then getAllElementsOfType(elist, typeName, {});
232+
case SCode.CLASS(name, _, _, _, SCode.R_PACKAGE(), SCode.PARTS(elist, _,_,_,_,_,_,_), _, _)
233+
equation
234+
nName = if(pathInProg=="")then name else pathInProg+"."+name;
235+
then getAllElementsOfType(elist, typeName, nName, {});
144236
case SCode.CLASS(_, _, _, _, _, SCode.PARTS(elist, _,_,_,_,_,_,_), _, _)
145237
equation
146238
(true) = isOfType(elist, typeName);
147-
148-
then {el};
239+
print ("Found a " + typeName + "\n");
240+
then {(el,pathInProg)};
149241
case _
150-
equation print("noName\n");
151-
// print(SCodeDump.unparseElementStr(el));
242+
equation
243+
// print("not of right type " + typeName + "\n");
244+
// print(SCodeDump.unparseElementStr(el) + "\n");
152245
then {};
153246
end matchcontinue;
154247
end getAllElementsOfType2;
155248

249+
156250
protected function isOfType
157251
input list<SCode.Element> elems;
158252
input String typeName;
@@ -225,7 +319,7 @@ output Absyn.Class out_vmodel;
225319
else
226320
GlobalScript.ISTMTS({GlobalScript.IEXP(exp, _)}, _) = Parser.parsestringexp(template);
227321
new_exp = parseAggregator(exp, Absyn.FUNCTIONARGS({Absyn.LIST(toExpList(out_es, {}))}, {}));
228-
// print("new TEMPLATE : " + Dump.dumpExpStr(new_exp) + "\n");
322+
//print("new TEMPLATE : " + Dump.dumpExpStr(new_exp) + "\n");
229323
out_class = updateClass(vmodel, typeSpec, {(new_exp, "")}, iname, env, false, {}, "");
230324
end if;
231325
then out_class;
@@ -368,9 +462,8 @@ algorithm
368462
list<Absyn.EquationItem> eqs1, eqs2;
369463
list<Absyn.ElementItem> elems1, elems2;
370464
Integer count;
371-
case(Absyn.PUBLIC(elems)) //TODO
465+
case(Absyn.PUBLIC(elems))
372466
equation
373-
// print("updating in parsePart Class\n");
374467
elems1 = parseElems(elems, defs, typeSpec, exp, instance_name, hasPreferred, preferred, path);
375468
then
376469
(Absyn.PUBLIC(elems1));
@@ -413,25 +506,26 @@ algorithm
413506
List<Mediator> m;
414507
case {}
415508
then in_elems;
416-
case (Absyn.ELEMENTITEM(Absyn.ELEMENT(finalPrefix,redeclareKeywords ,innerOuter, Absyn.COMPONENTS(attributes,tSpec, components), info , constrainClass))::rest)
509+
case (Absyn.ELEMENTITEM(Absyn.ELEMENT(finalPrefix,redeclareKeywords,innerOuter,
510+
Absyn.COMPONENTS(attributes,tSpec, components), info , constrainClass))::rest)
417511
algorithm
418512
_ := Absyn.typeSpecPath(typeSpec);
419-
// print ("*****************FINDING CLIENTS ... ");
420-
// print(Dump.unparseTypeSpec(typeSpec));
421-
// print(" + ");
422-
// print(Dump.unparseTypeSpec(tSpec));
423-
// print ("... \n");
513+
/*print ("*****************FINDING CLIENTS ... ");
514+
print(Dump.unparseTypeSpec(typeSpec));
515+
print(" + ");
516+
print(Dump.unparseTypeSpec(tSpec));
517+
print ("... \n");*/
424518
//if Interactive.isPrimitive(Absyn.pathToCref(path), defs) then fail(); end if;
425519

426520
if (Absyn.typeSpecPathString(typeSpec) == Absyn.typeSpecPathString(tSpec)) then
427-
print("Found provider \n");
521+
print("Found client" + Dump.unparseTypeSpec(typeSpec) + "\n");
428522
if(hasPreferred) then // handle preferred bindings
429523
e_list := applyModifiersPreferred(components, exp, instance_name, pathInClass, finalPrefix, redeclareKeywords ,innerOuter, info , constrainClass, attributes,tSpec, preferred);
430524
else
431525
e_list := applyModifiers(components, exp, instance_name, 0, finalPrefix, redeclareKeywords ,innerOuter, info , constrainClass, attributes,tSpec);
432526
end if;
433527
else
434-
print("NOT Found provider \n");
528+
//print("NOT Found provider \n");
435529
e_list := { Absyn.ELEMENTITEM(Absyn.ELEMENT(finalPrefix,redeclareKeywords ,innerOuter, Absyn.COMPONENTS(attributes,tSpec, components), info , constrainClass))};
436530

437531
end if;
@@ -924,11 +1018,11 @@ output list<Client_e> client_list;
9241018
protected
9251019
list<Absyn.ElementItem> e_items;
9261020
algorithm
927-
// print("Building instance list\n");
928-
// print("" + Dump.unparseClassStr(clazz) + "\n");
1021+
// print("Building instance list\n");
1022+
// print("" + Dump.unparseClassStr(clazz) + "\n");
9291023
e_items := Absyn.getElementItemsInClass(clazz);
9301024
client_list := parseElementInstList(e_items, env, NO_PRED(), mediators, client_list_in);
931-
print("DONE Building instance list\n");
1025+
// print("DONE Building instance list\n");
9321026
end buildInstList;
9331027

9341028

@@ -960,14 +1054,13 @@ algorithm
9601054
case (Absyn.ELEMENTITEM(Absyn.ELEMENT(_,_,_, Absyn.COMPONENTS(_,typeSpec, components), _, _))::rest)
9611055
algorithm
9621056
path := Absyn.typeSpecPath(typeSpec);
963-
// print ("TESTING in parseElementList ... ");
964-
// print(Dump.unparseTypeSpec(typeSpec));
965-
// print ("... \n");
1057+
/* print ("TESTING in parseElementList ... ");
1058+
print(Dump.unparseTypeSpec(typeSpec));
1059+
print ("... \n"); */
1060+
9661061
// if Interactive.isPrimitive(Absyn.pathToCref(path), env) then fail(); end if;
967-
// print("HERE\n");
968-
def := Interactive.getPathedClassInProgram(path,env); // load the element
1062+
def := Interactive.getPathedClassInProgram(path, env); // load the element
9691063
(isCl, iname, m) := isClient(Absyn.typeSpecPathString(typeSpec), mediators, {});
970-
//print("HERE" + iname + "\n");
9711064
if(isCl) then
9721065
new_predecessors := CLIENT_E(components, typeSpec, def, iname, predecessors, m);
9731066
l2 := new_predecessors::in_client_list;
@@ -1006,11 +1099,11 @@ algorithm
10061099
equation
10071100
//print("Testing mediator : " + mType + "\n");
10081101
(true, nm) = isClientInMediator(ci_name, clients);
1009-
// print("... found client : "+ ci_name +"\n");
1102+
print("... found client : "+ ci_name +"\n");
10101103
then (true, nm, MEDIATOR(mType, template, clients, providers, preferred)::in_m);
10111104
case _::rest
10121105
equation
1013-
// print("REST\n");
1106+
//print("REST\n");
10141107
then isClient(ci_name, rest, in_m);
10151108
end matchcontinue;
10161109
end isClient;
@@ -1052,7 +1145,7 @@ output List<Mediator> mediators_out;
10521145
local
10531146
list<SCode.Element> rest;
10541147
SCode.Element el;
1055-
List<Mediator> m;
1148+
List<Mediator> m;
10561149
case {} then mediators_in;
10571150
case el::rest
10581151
equation
@@ -1080,7 +1173,7 @@ algorithm
10801173
then getMediatorDefsElements(elist, {});
10811174
case SCode.CLASS(_, _, _, _, SCode.R_RECORD(_), SCode.PARTS(elist, _,_,_,_,_,_,_), _, _)
10821175
equation
1083-
(true, SOME(mod)) = isMediator(elist);
1176+
(true, SOME(mod)) = extendsType(elist, "Mediator");
10841177
Absyn.STRING(template) = getValue(mod, "template", "string");
10851178
str1 = System.stringReplace(template, "%", "");
10861179
str2 = System.stringReplace(str1, ":", "all");
@@ -1099,8 +1192,8 @@ algorithm
10991192

11001193
then {MEDIATOR(mType,str2, cls, prvs, pref)};
11011194
case _
1102-
equation print("noName\n");
1103-
// print(SCodeDump.unparseElementStr(el));
1195+
equation //print("noName\n");
1196+
//print(SCodeDump.unparseElementStr(el));
11041197
then {};
11051198
end matchcontinue;
11061199
end getMediatorDefsElement;
@@ -1213,25 +1306,30 @@ output String val;
12131306
end getArg;
12141307

12151308

1216-
protected function isMediator
1309+
protected function extendsType
12171310
input list<SCode.Element> elems;
1311+
input String typeName;
12181312
output Boolean result;
12191313
output Option<SCode.Mod> mods;
12201314
algorithm
1315+
12211316
(result, mods) := matchcontinue(elems)
12221317
local
12231318
list<SCode.Element> rest;
12241319
SCode.Element el;
12251320
Mediator m;
12261321
Absyn.Ident id;
12271322
SCode.Mod mod;
1323+
String tName;
12281324
case {} then (false, NONE());
1229-
case SCode.EXTENDS(Absyn.IDENT("Mediator"), _, mod, _, _)::_
1325+
case SCode.EXTENDS(Absyn.IDENT(tName), _, mod, _, _)::_
1326+
equation
1327+
true = (tName == typeName);
12301328
then (true, SOME(mod));
12311329
case _::rest
1232-
then isMediator(rest);
1330+
then extendsType(rest, typeName);
12331331
end matchcontinue;
1234-
end isMediator;
1332+
end extendsType;
12351333

12361334
protected function getValue
12371335
input SCode.Mod mod;

‎Compiler/Script/CevalScriptBackend.mo‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1110,6 +1110,19 @@ algorithm
11101110
print("failed inferBindings\n");
11111111
then (cache, Values.BOOL(false), st);
11121112

1113+
case (cache,_, "generateVerificationScenarios", {Values.CODE(Absyn.C_TYPENAME(classpath))},
1114+
(st as GlobalScript.SYMBOLTABLE(p as Absyn.PROGRAM())),_)
1115+
equation
1116+
pnew = Binding.generateVerificationScenarios(classpath, p);
1117+
newst = GlobalScriptUtil.setSymbolTableAST(st, pnew);
1118+
then
1119+
(cache,Values.BOOL(true), newst);
1120+
1121+
case (cache, _, "generateVerificationScenarios", _, st, _)
1122+
equation
1123+
print("failed to generateVerificationScenarios\n");
1124+
then (cache, Values.BOOL(false), st);
1125+
11131126
case (_,_, "rewriteBlockCall",{Values.CODE(Absyn.C_TYPENAME(classpath)), Values.CODE(Absyn.C_TYPENAME(path))},
11141127
(st as GlobalScript.SYMBOLTABLE(p as Absyn.PROGRAM())),_)
11151128
equation

0 commit comments

Comments
 (0)