Skip to content

Commit

Permalink
[NF] More fixes for checking when-clauses.
Browse files Browse the repository at this point in the history
- Handle all kinds of equations when checking when-clauses.
- Make the componentref set check more robust.
- Fix variability check for reinit.
- Do model verification after scalarization, it takes a negligible
  amount of time anyway.

Belonging to [master]:
  - OpenModelica/OMCompiler#3011
  - OpenModelica/OpenModelica-testsuite#1151
  • Loading branch information
perost authored and OpenModelica-Hudson committed Mar 28, 2019
1 parent adba422 commit b8d7e26
Show file tree
Hide file tree
Showing 3 changed files with 58 additions and 16 deletions.
4 changes: 2 additions & 2 deletions Compiler/NFFrontEnd/NFInst.mo
Expand Up @@ -161,8 +161,6 @@ algorithm
flat_model := SimplifyModel.simplify(flat_model);
funcs := Flatten.collectFunctions(flat_model, name);

VerifyModel.verify(flat_model);

// Collect package constants that couldn't be substituted with their values
// (e.g. because they where used with non-constant subscripts), and add them
// to the model.
Expand All @@ -176,6 +174,8 @@ algorithm
flat_model.variables := List.filterOnFalse(flat_model.variables, Variable.isEmptyArray);
end if;

VerifyModel.verify(flat_model);

// Convert the flat model to a DAE.
(dae, daeFuncs) := ConvertDAE.convert(flat_model, funcs, name, InstNode.info(inst_cls));

Expand Down
4 changes: 2 additions & 2 deletions Compiler/NFFrontEnd/NFTyping.mo
Expand Up @@ -2943,8 +2943,8 @@ algorithm

// The first argument must be a continuous time variable.
// Check the variability of the cref instead of the variability returned by
// typeExp, since expressions in when-equation count as discrete.
if ComponentRef.nodeVariability(cref) <> Variability.CONTINUOUS then
// typeExp, since expressions in when-equations count as discrete.
if ComponentRef.nodeVariability(cref) < Variability.IMPLICITLY_DISCRETE then
Error.addSourceMessage(Error.REINIT_MUST_BE_VAR,
{Expression.toString(crefExp),
Prefixes.variabilityString(ComponentRef.nodeVariability(cref))}, info);
Expand Down
66 changes: 54 additions & 12 deletions Compiler/NFFrontEnd/NFVerifyModel.mo
Expand Up @@ -41,6 +41,7 @@ protected
import ComponentRef = NFComponentRef;
import Equation = NFEquation;
import Expression = NFExpression;
import ExpandExp = NFExpandExp;

public
function verify
Expand Down Expand Up @@ -89,11 +90,7 @@ protected
Equation.Branch.BRANCH(body = body) := branch;
crefs2 := whenEquationBranchCrefs(body);

if not List.isEqualOnTrue(crefs1, crefs2, ComponentRef.isEqual) then
Error.addSourceMessage(Error.DIFFERENT_VARIABLES_SOLVED_IN_ELSEWHEN,
{}, ElementSource.getInfo(source));
fail();
end if;
checkCrefSetEquality(crefs1, crefs2, Error.DIFFERENT_VARIABLES_SOLVED_IN_ELSEWHEN, source);
end for;
end verifyWhenEquation;

Expand All @@ -105,8 +102,12 @@ protected
algorithm
for eq in eql loop
crefs := match eq
case Equation.EQUALITY() then whenEquationEqualityCrefs(eq.lhs, crefs);
case Equation.IF() then whenEquationIfCrefs(eq.branches, eq.source, crefs);
case Equation.EQUALITY() then whenEquationEqualityCrefs(eq.lhs, crefs);
case Equation.CREF_EQUALITY() then eq.lhs :: crefs;
case Equation.ARRAY_EQUALITY() then whenEquationEqualityCrefs(eq.lhs, crefs);
case Equation.REINIT() then whenEquationEqualityCrefs(eq.cref, crefs);
case Equation.IF() then whenEquationIfCrefs(eq.branches, eq.source, crefs);
else crefs;
end match;
end for;

Expand Down Expand Up @@ -144,15 +145,56 @@ protected
crefs2 := whenEquationBranchCrefs(body);

// All the branches must have the same set of crefs on the lhs.
if not List.isEqualOnTrue(crefs1, crefs2, ComponentRef.isEqual) then
Error.addSourceMessage(Error.WHEN_IF_VARIABLE_MISMATCH,
{}, ElementSource.getInfo(source));
fail();
end if;
checkCrefSetEquality(crefs1, crefs2, Error.WHEN_IF_VARIABLE_MISMATCH, source);
end for;

crefs := listAppend(crefs1, crefs);
end whenEquationIfCrefs;

function checkCrefSetEquality
input list<ComponentRef> crefs1;
input list<ComponentRef> crefs2;
input Error.Message errMsg;
input DAE.ElementSource source;
algorithm
// Assume the user isn't mixing different ways of subscripting array
// varibles in the different branches, and just check the sets as is.
if List.isEqualOnTrue(crefs1, crefs2, ComponentRef.isEqual) then
return;
end if;

// If the sets didn't match, expand arrays into scalars and try again.
if List.isEqualOnTrue(expandCrefSet(crefs1), expandCrefSet(crefs2), ComponentRef.isEqual) then
return;
end if;

// Couldn't get the sets to match, print an error and fail.
Error.addSourceMessage(errMsg, {}, ElementSource.getInfo(source));
fail();
end checkCrefSetEquality;

function expandCrefSet
input list<ComponentRef> crefs;
output list<ComponentRef> outCrefs = {};
protected
Expression exp;
list<Expression> expl;
algorithm
for cref in crefs loop
exp := Expression.fromCref(cref);
exp := ExpandExp.expandCref(exp);

if Expression.isArray(exp) then
expl := Expression.arrayElements(exp);
outCrefs := listAppend(list(Expression.toCref(e) for e in expl), outCrefs);
else
outCrefs := cref :: outCrefs;
end if;
end for;

outCrefs := List.sort(outCrefs, ComponentRef.isGreater);
outCrefs := List.sortedUnique(outCrefs, ComponentRef.isEqual);
end expandCrefSet;

annotation(__OpenModelica_Interface="frontend");
end NFVerifyModel;

0 comments on commit b8d7e26

Please sign in to comment.