OMCompiler/Compiler/NFFrontEnd/NFVerifyModel.mo
| Line | Branch | Exec | Source |
|---|---|---|---|
| 1 | /* | ||
| 2 | * This file is part of OpenModelica. | ||
| 3 | * | ||
| 4 | * Copyright (c) 1998-2026, Open Source Modelica Consortium (OSMC), | ||
| 5 | * c/o Linköpings universitet, Department of Computer and Information Science, | ||
| 6 | * SE-58183 Linköping, Sweden. | ||
| 7 | * | ||
| 8 | * All rights reserved. | ||
| 9 | * | ||
| 10 | * THIS PROGRAM IS PROVIDED UNDER THE TERMS OF AGPL VERSION 3 LICENSE OR | ||
| 11 | * THIS OSMC PUBLIC LICENSE (OSMC-PL) VERSION 1.8. | ||
| 12 | * ANY USE, REPRODUCTION OR DISTRIBUTION OF THIS PROGRAM CONSTITUTES | ||
| 13 | * RECIPIENT'S ACCEPTANCE OF THE OSMC PUBLIC LICENSE OR THE GNU AGPL | ||
| 14 | * VERSION 3, ACCORDING TO RECIPIENTS CHOICE. | ||
| 15 | * | ||
| 16 | * The OpenModelica software and the OSMC (Open Source Modelica Consortium) | ||
| 17 | * Public License (OSMC-PL) are obtained from OSMC, either from the above | ||
| 18 | * address, from the URLs: | ||
| 19 | * http://www.openmodelica.org or | ||
| 20 | * https://github.com/OpenModelica/ or | ||
| 21 | * http://www.ida.liu.se/projects/OpenModelica, | ||
| 22 | * and in the OpenModelica distribution. | ||
| 23 | * | ||
| 24 | * GNU AGPL version 3 is obtained from: | ||
| 25 | * https://www.gnu.org/licenses/licenses.html#GPL | ||
| 26 | * | ||
| 27 | * This program is distributed WITHOUT ANY WARRANTY; without | ||
| 28 | * even the implied warranty of MERCHANTABILITY or FITNESS | ||
| 29 | * FOR A PARTICULAR PURPOSE, EXCEPT AS EXPRESSLY SET FORTH | ||
| 30 | * IN THE BY RECIPIENT SELECTED SUBSIDIARY LICENSE CONDITIONS OF OSMC-PL. | ||
| 31 | * | ||
| 32 | * See the full OSMC Public License conditions for more details. | ||
| 33 | * | ||
| 34 | */ | ||
| 35 | |||
| 36 | encapsulated uniontype NFVerifyModel | ||
| 37 | import FlatModel = NFFlatModel; | ||
| 38 | |||
| 39 | protected | ||
| 40 | import List; | ||
| 41 | import Error; | ||
| 42 | import ErrorTypes; | ||
| 43 | import DAE; | ||
| 44 | import ElementSource; | ||
| 45 | import ExecStat.execStat; | ||
| 46 | import ComponentRef = NFComponentRef; | ||
| 47 | import Equation = NFEquation; | ||
| 48 | import Expression = NFExpression; | ||
| 49 | import ExpandExp = NFExpandExp; | ||
| 50 | import NFInstNode.InstNode; | ||
| 51 | import Record = NFRecord; | ||
| 52 | import Variable = NFVariable; | ||
| 53 | import Algorithm = NFAlgorithm; | ||
| 54 | import Statement = NFStatement; | ||
| 55 | import Binding = NFBinding; | ||
| 56 | import Subscript = NFSubscript; | ||
| 57 | import Dimension = NFDimension; | ||
| 58 | import Util; | ||
| 59 | import Type = NFType; | ||
| 60 | import NFPrefixes.Variability; | ||
| 61 | |||
| 62 | public | ||
| 63 | function verify | ||
| 64 | input FlatModel flatModel; | ||
| 65 | input Boolean isPartial; | ||
| 66 | algorithm | ||
| 67 |
2/2✓ Branch 0 taken 379715 times.
✓ Branch 1 taken 1571 times.
|
381286 | for var in flatModel.variables loop |
| 68 | 379715 | verifyVariable(var, isPartial); | |
| 69 | end for; | ||
| 70 | |||
| 71 |
2/2✓ Branch 0 taken 148468 times.
✓ Branch 1 taken 1569 times.
|
150037 | for eq in flatModel.equations loop |
| 72 | 148468 | verifyEquation(eq, isPartial); | |
| 73 | end for; | ||
| 74 | |||
| 75 |
2/2✓ Branch 0 taken 1899 times.
✓ Branch 1 taken 1569 times.
|
3468 | for ieq in flatModel.initialEquations loop |
| 76 | 1899 | verifyEquation(ieq, isPartial); | |
| 77 | end for; | ||
| 78 | |||
| 79 |
2/2✓ Branch 0 taken 144 times.
✓ Branch 1 taken 1569 times.
|
1713 | for alg in flatModel.algorithms loop |
| 80 | 144 | verifyAlgorithm(alg, isPartial); | |
| 81 | end for; | ||
| 82 | |||
| 83 |
2/2✓ Branch 0 taken 52 times.
✓ Branch 1 taken 1569 times.
|
1621 | for ialg in flatModel.initialAlgorithms loop |
| 84 | 52 | verifyAlgorithm(ialg, isPartial); | |
| 85 | end for; | ||
| 86 | |||
| 87 | // check for discrete real variables not assigned in when equations (#5836) | ||
| 88 |
2/2✓ Branch 0 taken 1567 times.
✓ Branch 1 taken 2 times.
|
1569 | if not isPartial then |
| 89 | 1567 | checkDiscreteReal(flatModel); | |
| 90 | end if; | ||
| 91 | |||
| 92 | 1569 | execStat(getInstanceName()); | |
| 93 | end verify; | ||
| 94 | |||
| 95 | protected | ||
| 96 | function verifyVariable | ||
| 97 | input Variable var; | ||
| 98 | input Boolean isPartial; | ||
| 99 | algorithm | ||
| 100 | 380160 | verifyBinding(var.binding, isPartial); | |
| 101 | |||
| 102 |
2/2✓ Branch 0 taken 642240 times.
✓ Branch 1 taken 380157 times.
|
1022397 | for attr in var.typeAttributes loop |
| 103 | 642240 | verifyBinding(Util.tuple22(attr), isPartial); | |
| 104 | end for; | ||
| 105 | |||
| 106 |
2/2✓ Branch 0 taken 445 times.
✓ Branch 1 taken 380157 times.
|
380602 | for v in var.children loop |
| 107 | 445 | verifyVariable(v, isPartial); | |
| 108 | end for; | ||
| 109 | end verifyVariable; | ||
| 110 | |||
| 111 | function verifyBinding | ||
| 112 | input Binding binding; | ||
| 113 | input Boolean isPartial; | ||
| 114 | algorithm | ||
| 115 |
2/2✓ Branch 1 taken 223947 times.
✓ Branch 2 taken 798453 times.
|
1022400 | if Binding.isBound(binding) then |
| 116 | 798453 | checkSubscriptBounds(Binding.getTypedExp(binding), isPartial, Binding.getInfo(binding)); | |
| 117 | end if; | ||
| 118 | end verifyBinding; | ||
| 119 | |||
| 120 | function verifyEquation | ||
| 121 | input Equation eq; | ||
| 122 | input Boolean isPartial; | ||
| 123 | algorithm | ||
| 124 | () := match eq | ||
| 125 | case Equation.WHEN() | ||
| 126 | guard not isPartial | ||
| 127 | algorithm | ||
| 128 | 319 | verifyWhenEquation(eq.branches, eq.source); | |
| 129 | then | ||
| 130 | (); | ||
| 131 | |||
| 132 | else (); | ||
| 133 | end match; | ||
| 134 | |||
| 135 |
2/2✓ Branch 1 taken 150363 times.
✓ Branch 2 taken 2 times.
|
300728 | Equation.applyExpShallow(eq, function checkSubscriptBounds(isPartial = isPartial, info = Equation.info(eq))); |
| 136 | end verifyEquation; | ||
| 137 | |||
| 138 | function verifyWhenEquation | ||
| 139 | "Checks that each branch in a when-equation has the same set of crefs on the lhs." | ||
| 140 | input list<Equation.Branch> branches; | ||
| 141 | input DAE.ElementSource source; | ||
| 142 | protected | ||
| 143 | list<ComponentRef> crefs1, crefs2; | ||
| 144 | list<Equation.Branch> rest_branches; | ||
| 145 | list<Equation> body; | ||
| 146 | algorithm | ||
| 147 | // Only when-equation with more than one branch needs to be checked. | ||
| 148 |
2/2✓ Branch 1 taken 287 times.
✓ Branch 2 taken 32 times.
|
319 | if List.hasOneElement(branches) then |
| 149 | 287 | return; | |
| 150 | end if; | ||
| 151 | |||
| 152 |
2/4✗ Branch 0 not taken.
✓ Branch 1 taken 32 times.
✗ Branch 3 not taken.
✓ Branch 4 taken 32 times.
|
32 | Equation.Branch.BRANCH(body = body) :: rest_branches := branches; |
| 153 | 32 | crefs1 := whenEquationBranchCrefs(body); | |
| 154 | |||
| 155 |
2/2✓ Branch 0 taken 41 times.
✓ Branch 1 taken 30 times.
|
71 | for branch in rest_branches loop |
| 156 |
1/2✗ Branch 0 not taken.
✓ Branch 1 taken 41 times.
|
41 | Equation.Branch.BRANCH(body = body) := branch; |
| 157 | 41 | crefs2 := whenEquationBranchCrefs(body); | |
| 158 | |||
| 159 | 41 | checkCrefSetEquality(crefs1, crefs2, Error.DIFFERENT_VARIABLES_SOLVED_IN_ELSEWHEN, source); | |
| 160 | end for; | ||
| 161 | end verifyWhenEquation; | ||
| 162 | |||
| 163 | function whenEquationBranchCrefs | ||
| 164 | "Helper function to verifyWhenEquation, returns the set of crefs that the | ||
| 165 | given list of equations contains on the lhs." | ||
| 166 | input list<Equation> eql; | ||
| 167 | output list<ComponentRef> crefs = {}; | ||
| 168 | algorithm | ||
| 169 |
5/5✓ Branch 0 taken 103 times.
✓ Branch 1 taken 3 times.
✓ Branch 2 taken 7 times.
✓ Branch 3 taken 113 times.
✓ Branch 4 taken 78 times.
|
191 | for eq in eql loop |
| 170 | crefs := match eq | ||
| 171 | 103 | case Equation.EQUALITY() then whenEquationEqualityCrefs(eq.lhs, crefs); | |
| 172 | 3 | case Equation.IF() then whenEquationIfCrefs(eq.branches, eq.source, crefs); | |
| 173 | else crefs; | ||
| 174 | end match; | ||
| 175 | end for; | ||
| 176 | |||
| 177 | 78 | crefs := List.sort(crefs, ComponentRef.isGreater); | |
| 178 | 78 | crefs := List.sortedUnique(crefs, ComponentRef.isEqual); | |
| 179 | end whenEquationBranchCrefs; | ||
| 180 | |||
| 181 | function whenEquationEqualityCrefs | ||
| 182 | input Expression lhsExp; | ||
| 183 | input output list<ComponentRef> crefs; | ||
| 184 | algorithm | ||
| 185 | crefs := match lhsExp | ||
| 186 | 103 | case Expression.CREF() then lhsExp.cref :: crefs; | |
| 187 | case Expression.TUPLE() | ||
| 188 | ✗ | then List.fold(lhsExp.elements, whenEquationEqualityCrefs, crefs); | |
| 189 | end match; | ||
| 190 | end whenEquationEqualityCrefs; | ||
| 191 | |||
| 192 | function whenEquationIfCrefs | ||
| 193 | "Checks that the left-hand sides of the given if-equation branches consists | ||
| 194 | of the same set of crefs, and adds that set to the given set of crefs." | ||
| 195 | input list<Equation.Branch> branches; | ||
| 196 | input DAE.ElementSource source; | ||
| 197 | input output list<ComponentRef> crefs; | ||
| 198 | protected | ||
| 199 | list<ComponentRef> crefs1, crefs2; | ||
| 200 | list<Equation.Branch> rest_branches; | ||
| 201 | list<Equation> body; | ||
| 202 | algorithm | ||
| 203 |
2/4✗ Branch 0 not taken.
✓ Branch 1 taken 3 times.
✗ Branch 3 not taken.
✓ Branch 4 taken 3 times.
|
3 | Equation.Branch.BRANCH(body = body) :: rest_branches := branches; |
| 204 | 3 | crefs1 := whenEquationBranchCrefs(body); | |
| 205 | |||
| 206 |
2/2✓ Branch 0 taken 2 times.
✓ Branch 1 taken 3 times.
|
5 | for branch in rest_branches loop |
| 207 |
1/2✗ Branch 0 not taken.
✓ Branch 1 taken 2 times.
|
2 | Equation.Branch.BRANCH(body = body) := branch; |
| 208 | 2 | crefs2 := whenEquationBranchCrefs(body); | |
| 209 | |||
| 210 | // All the branches must have the same set of crefs on the lhs. | ||
| 211 | 2 | checkCrefSetEquality(crefs1, crefs2, Error.WHEN_IF_VARIABLE_MISMATCH, source); | |
| 212 | end for; | ||
| 213 | |||
| 214 | 3 | crefs := listAppend(crefs1, crefs); | |
| 215 | end whenEquationIfCrefs; | ||
| 216 | |||
| 217 | function checkCrefSetEquality | ||
| 218 | input list<ComponentRef> crefs1; | ||
| 219 | input list<ComponentRef> crefs2; | ||
| 220 | input ErrorTypes.Message errMsg; | ||
| 221 | input DAE.ElementSource source; | ||
| 222 | algorithm | ||
| 223 | // Assume the user isn't mixing different ways of subscripting array | ||
| 224 | // varibles in the different branches, and just check the sets as is. | ||
| 225 |
2/2✓ Branch 1 taken 41 times.
✓ Branch 2 taken 2 times.
|
43 | if List.isEqualOnTrue(crefs1, crefs2, ComponentRef.isEqual) then |
| 226 | 41 | return; | |
| 227 | end if; | ||
| 228 | |||
| 229 | // If the sets didn't match, expand arrays into scalars and try again. | ||
| 230 |
1/2✗ Branch 3 not taken.
✓ Branch 4 taken 2 times.
|
2 | if List.isEqualOnTrue(expandCrefSet(crefs1), expandCrefSet(crefs2), ComponentRef.isEqual) then |
| 231 | ✗ | return; | |
| 232 | end if; | ||
| 233 | |||
| 234 | // Couldn't get the sets to match, print an error and fail. | ||
| 235 | 2 | Error.addSourceMessage(errMsg, {}, ElementSource.getInfo(source)); | |
| 236 | 2 | fail(); | |
| 237 | end checkCrefSetEquality; | ||
| 238 | |||
| 239 | function expandCrefSet | ||
| 240 | input list<ComponentRef> crefs; | ||
| 241 | output list<ComponentRef> outCrefs = {}; | ||
| 242 | protected | ||
| 243 | Expression exp; | ||
| 244 | array<Expression> expl; | ||
| 245 | algorithm | ||
| 246 |
2/2✓ Branch 0 taken 3 times.
✓ Branch 1 taken 4 times.
|
7 | for cref in crefs loop |
| 247 | 3 | exp := Expression.fromCref(cref); | |
| 248 | 3 | exp := ExpandExp.expandCref(exp); | |
| 249 | |||
| 250 |
1/2✗ Branch 1 not taken.
✓ Branch 2 taken 3 times.
|
3 | if Expression.isArray(exp) then |
| 251 | ✗ | expl := Expression.arrayElements(exp); | |
| 252 | ✗ | outCrefs := listAppend(list(Expression.toCref(e) for e in expl), outCrefs); | |
| 253 | else | ||
| 254 | outCrefs := cref :: outCrefs; | ||
| 255 | end if; | ||
| 256 | end for; | ||
| 257 | |||
| 258 | 4 | outCrefs := List.sort(outCrefs, ComponentRef.isGreater); | |
| 259 | 4 | outCrefs := List.sortedUnique(outCrefs, ComponentRef.isEqual); | |
| 260 | end expandCrefSet; | ||
| 261 | |||
| 262 | function verifyAlgorithm | ||
| 263 | input Algorithm alg; | ||
| 264 | input Boolean isPartial; | ||
| 265 | algorithm | ||
| 266 |
1/2✓ Branch 0 taken 196 times.
✗ Branch 1 not taken.
|
392 | Algorithm.apply(alg, function verifyStatement(isPartial = isPartial)); |
| 267 | end verifyAlgorithm; | ||
| 268 | |||
| 269 | function verifyStatement | ||
| 270 | input Statement stmt; | ||
| 271 | input Boolean isPartial; | ||
| 272 | algorithm | ||
| 273 |
1/2✓ Branch 1 taken 905 times.
✗ Branch 2 not taken.
|
1810 | Statement.applyExp(stmt, function checkSubscriptBounds(isPartial = isPartial, info = Statement.info(stmt))); |
| 274 | end verifyStatement; | ||
| 275 | |||
| 276 | function checkSubscriptBounds | ||
| 277 | input Expression exp; | ||
| 278 | input Boolean isPartial; | ||
| 279 | input SourceInfo info; | ||
| 280 | algorithm | ||
| 281 |
2/2✓ Branch 0 taken 1103764 times.
✓ Branch 1 taken 4 times.
|
2207532 | Expression.apply(exp, function checkSubscriptBounds_traverser(isPartial = isPartial, info = info)); |
| 282 | end checkSubscriptBounds; | ||
| 283 | |||
| 284 | function checkSubscriptBounds_traverser | ||
| 285 | input Expression exp; | ||
| 286 | input Boolean isPartial; | ||
| 287 | input SourceInfo info; | ||
| 288 | algorithm | ||
| 289 | () := match exp | ||
| 290 | case Expression.CREF() | ||
| 291 | algorithm | ||
| 292 | 467641 | checkSubscriptBoundsCref(exp.cref, isPartial, info); | |
| 293 | then | ||
| 294 | (); | ||
| 295 | |||
| 296 | else (); | ||
| 297 | end match; | ||
| 298 | end checkSubscriptBounds_traverser; | ||
| 299 | |||
| 300 | function checkSubscriptBoundsCref | ||
| 301 | input ComponentRef cref; | ||
| 302 | input Boolean isPartial; | ||
| 303 | input SourceInfo info; | ||
| 304 | algorithm | ||
| 305 | () := match cref | ||
| 306 | local | ||
| 307 | list<Dimension> dims; | ||
| 308 | list<Subscript> subs; | ||
| 309 | Dimension d; | ||
| 310 | Integer int_sub, index; | ||
| 311 | |||
| 312 | case ComponentRef.CREF(subscripts = subs as _ :: _, ty = Type.ARRAY(dimensions = dims)) | ||
| 313 | algorithm | ||
| 314 | index := 1; | ||
| 315 | |||
| 316 |
2/2✓ Branch 0 taken 258886 times.
✓ Branch 1 taken 207524 times.
|
466410 | for s in subs loop |
| 317 |
1/2✗ Branch 0 not taken.
✓ Branch 1 taken 258886 times.
|
258886 | d :: dims := dims; |
| 318 | |||
| 319 |
4/4✓ Branch 1 taken 256760 times.
✓ Branch 2 taken 2126 times.
✓ Branch 4 taken 256759 times.
✓ Branch 5 taken 1 time.
|
258886 | if Subscript.isScalarLiteral(s) and Dimension.isKnown(d) then |
| 320 | 256759 | int_sub := Subscript.toInteger(s); | |
| 321 | |||
| 322 |
3/4✓ Branch 0 taken 256759 times.
✗ Branch 1 not taken.
✓ Branch 3 taken 4 times.
✓ Branch 4 taken 256755 times.
|
256759 | if int_sub < 1 or int_sub > Dimension.size(d) then |
| 323 | 16 | Error.addSourceMessage(Error.ARRAY_INDEX_OUT_OF_BOUNDS, | |
| 324 | {Subscript.toString(s), String(index), | ||
| 325 | Dimension.toString(d), ComponentRef.firstName(cref)}, info); | ||
| 326 | |||
| 327 |
2/2✓ Branch 0 taken 3 times.
✓ Branch 1 taken 1 time.
|
4 | if not isPartial then |
| 328 | 3 | fail(); | |
| 329 | end if; | ||
| 330 | end if; | ||
| 331 | end if; | ||
| 332 | |||
| 333 | 258883 | index := index + 1; | |
| 334 | end for; | ||
| 335 | |||
| 336 | 207524 | checkSubscriptBoundsCref(cref.restCref, isPartial, info); | |
| 337 | then | ||
| 338 | (); | ||
| 339 | |||
| 340 | else (); | ||
| 341 | end match; | ||
| 342 | end checkSubscriptBoundsCref; | ||
| 343 | |||
| 344 | function checkDiscreteReal | ||
| 345 | "author: kabdelhak 2020-06 | ||
| 346 | Checks if all discrete real variables are defined by a when-statement. | ||
| 347 | Linear with respect to the number of equations and variables. It traverses | ||
| 348 | each equation and collects all relevant component references and afterwards | ||
| 349 | checks if any discrete real variables were not defined by a when-statement. | ||
| 350 | Ticket: #5836" | ||
| 351 | input FlatModel flatModel; | ||
| 352 | protected | ||
| 353 | UnorderedSet<ComponentRef> discrete_reals; | ||
| 354 | list<Variable> illegal_discrete_vars = {}; | ||
| 355 | algorithm | ||
| 356 | // use hash and equality that ignores subscripts to handle arrays | ||
| 357 | 1567 | discrete_reals := UnorderedSet.new(ComponentRef.hashStrip, ComponentRef.isEqualStrip); | |
| 358 | |||
| 359 | // collect all lhs crefs that are discrete and real from equations | ||
| 360 |
2/2✓ Branch 0 taken 148464 times.
✓ Branch 1 taken 1567 times.
|
150031 | for eqn in flatModel.equations loop |
| 361 | 148464 | checkDiscreteRealEquation(eqn, discrete_reals, false); | |
| 362 | end for; | ||
| 363 | |||
| 364 | // collect all lhs crefs that are discrete and real from algorithms | ||
| 365 |
2/2✓ Branch 0 taken 144 times.
✓ Branch 1 taken 1567 times.
|
1711 | for alg in flatModel.algorithms loop |
| 366 |
2/2✓ Branch 0 taken 296 times.
✓ Branch 1 taken 144 times.
|
440 | for statement in alg.statements loop |
| 367 | 296 | checkDiscreteRealStatement(statement, discrete_reals, false); | |
| 368 | end for; | ||
| 369 | end for; | ||
| 370 | |||
| 371 | // check if all discrete real variables are assigned in when bodys | ||
| 372 |
2/2✓ Branch 0 taken 379697 times.
✓ Branch 1 taken 1567 times.
|
381264 | for variable in flatModel.variables loop |
| 373 | // check variability and not type for discrete variables | ||
| 374 |
5/6✓ Branch 1 taken 300 times.
✓ Branch 2 taken 379397 times.
✓ Branch 5 taken 181 times.
✓ Branch 6 taken 119 times.
✗ Branch 8 not taken.
✓ Branch 9 taken 181 times.
|
379697 | if Variable.variability(variable) == Variability.DISCRETE and Type.isReal(Type.arrayElementType(variable.ty)) and |
| 375 | not UnorderedSet.contains(variable.name, discrete_reals) then | ||
| 376 | illegal_discrete_vars := variable :: illegal_discrete_vars; | ||
| 377 | end if; | ||
| 378 | end for; | ||
| 379 | |||
| 380 | // report error if there are any | ||
| 381 |
1/2✗ Branch 0 not taken.
✓ Branch 1 taken 1567 times.
|
1567 | if not listEmpty(illegal_discrete_vars) then |
| 382 | ✗ | for var in illegal_discrete_vars loop | |
| 383 | ✗ | Error.addSourceMessage(Error.DISCRETE_REAL_UNDEFINED, | |
| 384 | {ComponentRef.toString(ComponentRef.stripSubscriptsAll(var.name))}, var.info); | ||
| 385 | end for; | ||
| 386 | ✗ | fail(); | |
| 387 | end if; | ||
| 388 | end checkDiscreteReal; | ||
| 389 | |||
| 390 | protected | ||
| 391 | function checkDiscreteRealBranch | ||
| 392 | "author: kabdelhak 2020-06 | ||
| 393 | collects all single discrete real crefs on the LHS of the body eqns of a | ||
| 394 | when (or nested if inside when) branch." | ||
| 395 | input Equation.Branch branch; | ||
| 396 | input output UnorderedSet<ComponentRef> discreteReals; | ||
| 397 | input Boolean when_found; | ||
| 398 | algorithm | ||
| 399 | () := match branch | ||
| 400 | case Equation.BRANCH() guard(when_found) | ||
| 401 | algorithm | ||
| 402 |
2/2✓ Branch 0 taken 565 times.
✓ Branch 1 taken 370 times.
|
935 | for eqn in branch.body loop |
| 403 | 565 | checkDiscreteRealEquation(eqn, discreteReals, when_found); | |
| 404 | end for; | ||
| 405 | then | ||
| 406 | (); | ||
| 407 | |||
| 408 | else (); | ||
| 409 | end match; | ||
| 410 | end checkDiscreteRealBranch; | ||
| 411 | |||
| 412 | function checkDiscreteRealEquation | ||
| 413 | "author: kabdelhak 2020-06 | ||
| 414 | collects all single discrete real crefs on the LHS of a branch which is | ||
| 415 | part of a when eqn body. Only use to analyze when equation bodys!" | ||
| 416 | input Equation body_eqn; | ||
| 417 | input UnorderedSet<ComponentRef> discreteReals; | ||
| 418 | input Boolean when_found; | ||
| 419 | algorithm | ||
| 420 | () := match body_eqn | ||
| 421 | local | ||
| 422 | Expression lhs; | ||
| 423 | list<Equation> body; | ||
| 424 | list<Equation.Branch> branches; | ||
| 425 | |||
| 426 | case Equation.EQUALITY(lhs = lhs) | ||
| 427 | guard(when_found) | ||
| 428 | algorithm | ||
| 429 | 509 | checkDiscreteRealExp(lhs, discreteReals); | |
| 430 | then | ||
| 431 | (); | ||
| 432 | |||
| 433 | // traverse nested if equations. It suffices if the variable is defined in ANY branch. | ||
| 434 | case Equation.IF(branches = branches) | ||
| 435 | algorithm | ||
| 436 |
2/2✓ Branch 0 taken 567 times.
✓ Branch 1 taken 168 times.
|
735 | for branch in branches loop |
| 437 | 567 | checkDiscreteRealBranch(branch, discreteReals, when_found); | |
| 438 | end for; | ||
| 439 | then | ||
| 440 | (); | ||
| 441 | |||
| 442 | // traverse when body | ||
| 443 | case Equation.WHEN(branches = branches) | ||
| 444 | algorithm | ||
| 445 |
2/2✓ Branch 0 taken 357 times.
✓ Branch 1 taken 318 times.
|
675 | for branch in branches loop |
| 446 | 357 | checkDiscreteRealBranch(branch, discreteReals, true); | |
| 447 | end for; | ||
| 448 | then | ||
| 449 | (); | ||
| 450 | |||
| 451 | // what if LHS is indexed? :( | ||
| 452 | case Equation.FOR(body = body) | ||
| 453 | algorithm | ||
| 454 |
2/2✓ Branch 0 taken 290 times.
✓ Branch 1 taken 269 times.
|
559 | for eqn in body loop |
| 455 | 290 | checkDiscreteRealEquation(eqn, discreteReals, when_found); | |
| 456 | end for; | ||
| 457 | then | ||
| 458 | (); | ||
| 459 | |||
| 460 | else (); | ||
| 461 | end match; | ||
| 462 | end checkDiscreteRealEquation; | ||
| 463 | |||
| 464 | function checkDiscreteRealStatement | ||
| 465 | "author: kabdelhak 2020-06 | ||
| 466 | collects all single discrete real crefs on the LHS of a statement which is | ||
| 467 | part of a when algorithm body." | ||
| 468 | input Statement statement; | ||
| 469 | input UnorderedSet<ComponentRef> discreteReals; | ||
| 470 | input Boolean when_found; | ||
| 471 | algorithm | ||
| 472 | () := match statement | ||
| 473 | local | ||
| 474 | Expression lhs; | ||
| 475 | list<tuple<Expression, list<Statement>>> branches; | ||
| 476 | list<Statement> body; | ||
| 477 | |||
| 478 | case Statement.WHEN(branches = branches) | ||
| 479 | algorithm | ||
| 480 |
2/2✓ Branch 0 taken 118 times.
✓ Branch 1 taken 82 times.
|
200 | for branch in branches loop |
| 481 | 118 | (_, body) := branch; | |
| 482 |
2/2✓ Branch 0 taken 191 times.
✓ Branch 1 taken 118 times.
|
309 | for statement in body loop |
| 483 | 191 | checkDiscreteRealStatement(statement, discreteReals, true); | |
| 484 | end for; | ||
| 485 | end for; | ||
| 486 | then | ||
| 487 | (); | ||
| 488 | |||
| 489 | case Statement.ASSIGNMENT(lhs = lhs) guard(when_found) | ||
| 490 | algorithm | ||
| 491 | 183 | checkDiscreteRealExp(lhs, discreteReals); | |
| 492 | then | ||
| 493 | (); | ||
| 494 | |||
| 495 | // traverse nested if Algorithms. It suffices if the variable is defined in ANY branch. | ||
| 496 | case Statement.IF(branches = branches) | ||
| 497 | algorithm | ||
| 498 |
2/2✓ Branch 0 taken 169 times.
✓ Branch 1 taken 132 times.
|
301 | for branch in branches loop |
| 499 | 169 | (_, body) := branch; | |
| 500 |
2/2✓ Branch 0 taken 175 times.
✓ Branch 1 taken 169 times.
|
344 | for stmt in body loop |
| 501 | 175 | checkDiscreteRealStatement(stmt, discreteReals, when_found); | |
| 502 | end for; | ||
| 503 | end for; | ||
| 504 | then | ||
| 505 | (); | ||
| 506 | |||
| 507 | // what if the LHS is indexed? :( | ||
| 508 | case Statement.FOR(body = body) | ||
| 509 | algorithm | ||
| 510 |
2/2✓ Branch 0 taken 82 times.
✓ Branch 1 taken 74 times.
|
156 | for statement in body loop |
| 511 | 82 | checkDiscreteRealStatement(statement, discreteReals, when_found); | |
| 512 | end for; | ||
| 513 | then | ||
| 514 | (); | ||
| 515 | |||
| 516 | else (); | ||
| 517 | end match; | ||
| 518 | end checkDiscreteRealStatement; | ||
| 519 | |||
| 520 | function checkDiscreteRealExp | ||
| 521 | "author: kabdelhak 2020-06 | ||
| 522 | collects all single discrete real crefs of an expression which represents the LHS." | ||
| 523 | input Expression exp; | ||
| 524 | input UnorderedSet<ComponentRef> discreteReals; | ||
| 525 | algorithm | ||
| 526 | () := match exp | ||
| 527 | local | ||
| 528 | Type ty; | ||
| 529 | ComponentRef cref; | ||
| 530 | list<Expression> elements; | ||
| 531 | InstNode cls; | ||
| 532 | |||
| 533 | // only add if it is a real variable, we cannot check for discrete here | ||
| 534 | // since only the variable has variablity information | ||
| 535 | // Type.isDiscrete does always return false for REAL | ||
| 536 | case Expression.CREF(ty = ty, cref = cref) | ||
| 537 | guard(Type.isReal(Type.arrayElementType(ty))) | ||
| 538 | algorithm | ||
| 539 | 372 | UnorderedSet.add(cref, discreteReals); | |
| 540 | then | ||
| 541 | (); | ||
| 542 | |||
| 543 | case Expression.CREF(ty = ty as Type.COMPLEX(), cref = cref) | ||
| 544 | guard(Type.isRecord(ty)) | ||
| 545 | algorithm | ||
| 546 | ✗ | checkDiscreteRealRecord(cref, Type.complexNode(ty), discreteReals); | |
| 547 | then | ||
| 548 | (); | ||
| 549 | |||
| 550 | case Expression.TUPLE(elements = elements) | ||
| 551 | algorithm | ||
| 552 |
2/2✓ Branch 0 taken 42 times.
✓ Branch 1 taken 14 times.
|
56 | for element in elements loop |
| 553 | 42 | checkDiscreteRealExp(element, discreteReals); | |
| 554 | end for; | ||
| 555 | then | ||
| 556 | (); | ||
| 557 | |||
| 558 | else (); | ||
| 559 | end match; | ||
| 560 | end checkDiscreteRealExp; | ||
| 561 | |||
| 562 | function checkDiscreteRealRecord | ||
| 563 | input ComponentRef cref; | ||
| 564 | input InstNode cls; | ||
| 565 | input UnorderedSet<ComponentRef> discreteReals; | ||
| 566 | protected | ||
| 567 | ComponentRef element; | ||
| 568 | list<InstNode> inputs; | ||
| 569 | algorithm | ||
| 570 | ✗ | UnorderedSet.add(cref, discreteReals); | |
| 571 | // also add all record elements | ||
| 572 | ✗ | (inputs, _, _) := Record.collectRecordParams(cls); | |
| 573 | ✗ | for node in inputs loop | |
| 574 | ✗ | element := ComponentRef.prefixCref(node, InstNode.getType(node), {}, cref); | |
| 575 | ✗ | UnorderedSet.add(element, discreteReals); | |
| 576 | end for; | ||
| 577 | end checkDiscreteRealRecord; | ||
| 578 | |||
| 579 | annotation(__OpenModelica_Interface="nf_frontend"); | ||
| 580 | end NFVerifyModel; | ||
| 581 |