Skip to content

Commit

Permalink
[NF] update discrete variable verification (#8476)
Browse files Browse the repository at this point in the history
- broke for -nfScalarize
 - fixed nesting of function to also catch when equations and statemens inside of if and for equations/statements
  • Loading branch information
kabdelhak committed Jan 27, 2022
1 parent 9651533 commit 68fa35a
Show file tree
Hide file tree
Showing 2 changed files with 39 additions and 56 deletions.
85 changes: 34 additions & 51 deletions OMCompiler/Compiler/NFFrontEnd/NFVerifyModel.mo
Expand Up @@ -342,19 +342,7 @@ protected
algorithm
// collect all lhs crefs that are discrete and real from equations
for eqn in flatModel.equations loop
hashTable := match eqn
local
list<Equation.Branch> branches;

case Equation.WHEN(branches = branches)
algorithm
for branch in branches loop
hashTable := checkDiscreteRealBranch(branch, hashTable);
end for;
then hashTable;

else hashTable;
end match;
hashTable := checkDiscreteRealEquation(eqn, hashTable, false);
end for;

// collect all lhs crefs that are discrete and real from algorithms
Expand All @@ -366,7 +354,7 @@ protected
case Algorithm.ALGORITHM(statements = statements)
algorithm
for statement in statements loop
hashTable := checkDiscreteRealStatement(statement, hashTable);
hashTable := checkDiscreteRealStatement(statement, hashTable, false);
end for;
then hashTable;

Expand Down Expand Up @@ -400,28 +388,30 @@ protected
when (or nested if inside when) branch."
input Equation.Branch branch;
input output HashTable hashTable;
input Boolean when_found;
algorithm
hashTable := match branch
local
list<Equation> body;

case Equation.BRANCH(body = body)
case Equation.BRANCH(body = body) guard(when_found)
algorithm
for eqn in body loop
hashTable := checkDiscreteRealBranchBodyEqn(eqn, hashTable);
hashTable := checkDiscreteRealEquation(eqn, hashTable, when_found);
end for;
then hashTable;

else hashTable;
end match;
end checkDiscreteRealBranch;

function checkDiscreteRealBranchBodyEqn
function checkDiscreteRealEquation
"author: kabdelhak 2020-06
collects all single discrete real crefs on the LHS of a branch which is
part of a when eqn body. Only use to analyze when equation bodys!"
input Equation body_eqn;
input output HashTable hashTable;
input Boolean when_found;
algorithm
hashTable := match body_eqn
local
Expand All @@ -432,86 +422,79 @@ protected
list<Equation> body;
list<Equation.Branch> branches;

case Equation.EQUALITY(lhs = lhs) then checkDiscreteRealExp(lhs, hashTable);
case Equation.ARRAY_EQUALITY(lhs = lhs) then checkDiscreteRealExp(lhs, hashTable);
case Equation.EQUALITY(lhs = lhs) guard(when_found) then checkDiscreteRealExp(lhs, hashTable);
case Equation.ARRAY_EQUALITY(lhs = lhs) guard(when_found) then checkDiscreteRealExp(lhs, hashTable);

case Equation.CREF_EQUALITY(lhs = cref as ComponentRef.CREF(ty = ty)) guard(Type.isRealRecursive(ty))
case Equation.CREF_EQUALITY(lhs = cref as ComponentRef.CREF(ty = ty)) guard(Type.isRealRecursive(ty) and when_found)
algorithm
// remove all subscripts to handle arrays
hashTable := BaseHashTable.add((ComponentRef.stripSubscriptsAll(cref), 0), hashTable);
then hashTable;

case Equation.CREF_EQUALITY(lhs = cref as ComponentRef.CREF(ty = ty as Type.COMPLEX(cls = cls))) guard(Type.isRecord(ty))
case Equation.CREF_EQUALITY(lhs = cref as ComponentRef.CREF(ty = ty as Type.COMPLEX(cls = cls))) guard(Type.isRecord(ty) and when_found)
then checkDiscreteRealRecord(cref, cls, hashTable);

// traverse nested if equations. It suffices if the variable is defined in ANY branch.
case Equation.IF(branches = branches)
algorithm
for branch in branches loop
hashTable := checkDiscreteRealBranch(branch, hashTable);
hashTable := checkDiscreteRealBranch(branch, hashTable, when_found);
end for;
then hashTable;

// traverse when body
case Equation.WHEN(branches = branches)
algorithm
for branch in branches loop
hashTable := checkDiscreteRealBranch(branch, hashTable, true);
end for;
then hashTable;

// what if LHS is indexed? :(
case Equation.FOR(body = body)
algorithm
for eqn in body loop
hashTable := checkDiscreteRealBranchBodyEqn(eqn, hashTable);
hashTable := checkDiscreteRealEquation(eqn, hashTable, when_found);
end for;
then hashTable;

else hashTable;
end match;
end checkDiscreteRealBranchBodyEqn;
end checkDiscreteRealEquation;

function checkDiscreteRealStatement
"author: kabdelhak 2020-06
collects all single discrete real crefs on the LHS of the body statements of
a when algorithm."
collects all single discrete real crefs on the LHS of a statement which is
part of a when algorithm body."
input Statement statement;
input output HashTable hashTable;
input Boolean when_found;
algorithm
hashTable := match statement
local
Expression lhs;
list<tuple<Expression, list<Statement>>> branches;
list<Statement> body_statements;
list<Statement> body;

case Statement.WHEN(branches = branches)
algorithm
for branch in branches loop
(_, body_statements) := branch;
for statement in body_statements loop
hashTable := checkDiscreteRealBodyStatement(statement, hashTable);
(_, body) := branch;
for statement in body loop
hashTable := checkDiscreteRealStatement(statement, hashTable, true);
end for;
end for;
then hashTable;

else hashTable;
end match;
end checkDiscreteRealStatement;

function checkDiscreteRealBodyStatement
"author: kabdelhak 2020-06
collects all single discrete real crefs on the LHS of a statement which is
part of a when algorithm body. Only use to analyze when algorithm bodys!"
input Statement statement;
input output HashTable hashTable;
algorithm
hashTable := match statement
local
Expression lhs;
list<tuple<Expression, list<Statement>>> branches;
list<Statement> body;

case Statement.ASSIGNMENT(lhs = lhs) then checkDiscreteRealExp(lhs, hashTable);
case Statement.ASSIGNMENT(lhs = lhs) guard(when_found) then checkDiscreteRealExp(lhs, hashTable);

// traverse nested if Algorithms. It suffices if the variable is defined in ANY branch.
case Statement.IF(branches = branches)
algorithm
for branch in branches loop
(_, body) := branch;
for stmt in body loop
hashTable := checkDiscreteRealBodyStatement(stmt, hashTable);
hashTable := checkDiscreteRealStatement(stmt, hashTable, when_found);
end for;
end for;
then hashTable;
Expand All @@ -520,13 +503,13 @@ protected
case Statement.FOR(body = body)
algorithm
for statement in body loop
hashTable := checkDiscreteRealBodyStatement(statement, hashTable);
hashTable := checkDiscreteRealStatement(statement, hashTable, when_found);
end for;
then hashTable;

else hashTable;
end match;
end checkDiscreteRealBodyStatement;
end checkDiscreteRealStatement;

function checkDiscreteRealExp
"author: kabdelhak 2020-06
Expand Down
10 changes: 5 additions & 5 deletions OMCompiler/Compiler/Util/List.mo
Expand Up @@ -6498,11 +6498,11 @@ public function toString<T>
"
input list<T> inList;
input FuncType inPrintFunc;
input String inListNameStr "The name of the list.";
input String inBeginStr "The start of the list";
input String inDelimitStr "The delimiter between list elements.";
input String inEndStr "The end of the list.";
input Boolean inPrintEmpty "If false, don't output begin and end if the list is empty.";
input String inListNameStr = "" "The name of the list." ;
input String inBeginStr = "{" "The start of the list";
input String inDelimitStr = ", " "The delimiter between list elements.";
input String inEndStr = "}" "The end of the list.";
input Boolean inPrintEmpty = true "If false, don't output begin and end if the list is empty.";
output String outString;

partial function FuncType
Expand Down

0 comments on commit 68fa35a

Please sign in to comment.