OMCompiler/Compiler/NFFrontEnd/NFStateMachineFlatten.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 package NFStateMachineFlatten | ||
| 37 | "Transform state machines in the NF FlatModel to flat data-flow equations. | ||
| 38 | This is the NF equivalent of StateMachineFlatten.mo, operating on NFFlatModel | ||
| 39 | instead of DAE. Implements the transformation described in MLS §17." | ||
| 40 | |||
| 41 | import FlatModel = NFFlatModel; | ||
| 42 | import Equation = NFEquation; | ||
| 43 | import Expression = NFExpression; | ||
| 44 | import Type = NFType; | ||
| 45 | import ComponentRef = NFComponentRef; | ||
| 46 | import Variable = NFVariable; | ||
| 47 | import Binding = NFBinding; | ||
| 48 | import Attributes = NFAttributes; | ||
| 49 | import Dimension = NFDimension; | ||
| 50 | import Subscript = NFSubscript; | ||
| 51 | import Operator = NFOperator; | ||
| 52 | |||
| 53 | protected | ||
| 54 | import Call = NFCall; | ||
| 55 | import DAE; | ||
| 56 | import ElementSource; | ||
| 57 | import Error; | ||
| 58 | import ExecStat.execStat; | ||
| 59 | import List; | ||
| 60 | import NFBackendExtension; | ||
| 61 | import NFBuiltinFuncs; | ||
| 62 | import NFInstNode.InstNode; | ||
| 63 | import NFInstNode; | ||
| 64 | import NFPrefixes.{Variability, Purity, Visibility}; | ||
| 65 | import SCode; | ||
| 66 | import UnorderedMap; | ||
| 67 | import NFEquation.ScalarizeMode; | ||
| 68 | |||
| 69 | |||
| 70 | // ============================================================ | ||
| 71 | // Internal data types | ||
| 72 | // ============================================================ | ||
| 73 | |||
| 74 | protected | ||
| 75 | uniontype Transition | ||
| 76 | record TRANSITION | ||
| 77 | Integer from; | ||
| 78 | Integer to; | ||
| 79 | Expression condition; | ||
| 80 | Boolean immediate = true; | ||
| 81 | Boolean reset = true; | ||
| 82 | Boolean synchronize = false; | ||
| 83 | Integer priority = 1; | ||
| 84 | end TRANSITION; | ||
| 85 | end Transition; | ||
| 86 | |||
| 87 | protected | ||
| 88 | uniontype FlatSmSemantics | ||
| 89 | record FLAT_SM_SEMANTICS | ||
| 90 | ComponentRef initStateRef "Cref of the initial state (used as prefix for smOf vars)"; | ||
| 91 | array<ComponentRef> smComps "State crefs; index 1 = initial state"; | ||
| 92 | list<Transition> t "Transitions sorted by priority"; | ||
| 93 | list<Expression> c "Conditions sorted by priority"; | ||
| 94 | list<Variable> vars "SMS discrete variables"; | ||
| 95 | list<Variable> knowns "SMS parameters/constants"; | ||
| 96 | list<Equation> eqs "SMS equations"; | ||
| 97 | list<Variable> pvars "Propagation variables"; | ||
| 98 | list<Equation> peqs "Propagation equations"; | ||
| 99 | Option<ComponentRef> enclosingState "Enclosing state if hierarchical SM"; | ||
| 100 | end FLAT_SM_SEMANTICS; | ||
| 101 | end FlatSmSemantics; | ||
| 102 | |||
| 103 | constant String SMS_PRE = "smOf"; | ||
| 104 | |||
| 105 | // ============================================================ | ||
| 106 | // Public entry point | ||
| 107 | // ============================================================ | ||
| 108 | |||
| 109 | public | ||
| 110 | function flatten | ||
| 111 | "Main entry point. Transforms state machine NORETCALL equations to flat data-flow equations." | ||
| 112 | input output FlatModel flatModel; | ||
| 113 | protected | ||
| 114 | type OuterVarList = list<tuple<ComponentRef, ComponentRef>>; | ||
| 115 | list<ComponentRef> initStates; | ||
| 116 | list<list<ComponentRef>> smGroups; | ||
| 117 | list<Equation> smEqs, otherEqs, resultEqs; | ||
| 118 | list<Variable> smVars, resultVars; | ||
| 119 | list<ComponentRef> allStateCrefs; | ||
| 120 | UnorderedMap<ComponentRef, OuterVarList> outerVarMap; | ||
| 121 | // Hierarchy detection: map from stateCref → semantics of SM it belongs to | ||
| 122 | UnorderedMap<ComponentRef, FlatSmSemantics> stateToSem; | ||
| 123 | list<tuple<ComponentRef, list<ComponentRef>>> smGroupPairs, smGroupsSorted; | ||
| 124 | FlatSmSemantics sem; | ||
| 125 | ComponentRef initState, parentPrefix; | ||
| 126 | list<ComponentRef> stateCrefs; | ||
| 127 | Option<ComponentRef> enclosingStateCrefOpt; | ||
| 128 | Option<FlatSmSemantics> enclosingSmSemOpt; | ||
| 129 | algorithm | ||
| 130 | // Quick exit if no state machines present | ||
| 131 | // initialState() lives in initialEquations; transition() in equations | ||
| 132 |
3/4✓ Branch 1 taken 1432 times.
✓ Branch 2 taken 3 times.
✓ Branch 4 taken 1432 times.
✗ Branch 5 not taken.
|
1435 | if not List.any(flatModel.equations, isTransitionOrInitialState) and |
| 133 | not List.any(flatModel.initialEquations, isTransitionOrInitialState) then | ||
| 134 | 1432 | return; | |
| 135 | end if; | ||
| 136 | |||
| 137 | // Partition: initialState() from initialEquations, transition() from equations | ||
| 138 | 3 | (initStates, smGroups) := groupStateMachines(flatModel.equations, flatModel.initialEquations); | |
| 139 | |||
| 140 |
1/2✗ Branch 0 not taken.
✓ Branch 1 taken 3 times.
|
3 | if listEmpty(initStates) then |
| 141 | ✗ | return; | |
| 142 | end if; | ||
| 143 | |||
| 144 | // Collect all state crefs across all SM groups | ||
| 145 | 3 | allStateCrefs := List.flatten(smGroups); | |
| 146 | |||
| 147 | // Remove SM equations and outer-state equations from otherEqs | ||
| 148 | // (outer-state equations are those whose scope matches a state component name) | ||
| 149 | 3 | otherEqs := List.filterOnFalse(flatModel.equations, isTransitionOrInitialState); | |
| 150 | 3 | otherEqs := List.filterOnFalse(otherEqs, | |
| 151 | function isOuterStateEquation(stateCrefs = allStateCrefs)); | ||
| 152 | |||
| 153 | // outerVarMap collects: outer var → [(activeRef, perStateVar)] for merge equation generation | ||
| 154 | 3 | outerVarMap := UnorderedMap.new<OuterVarList>( | |
| 155 | ComponentRef.hash, ComponentRef.isEqual); | ||
| 156 | |||
| 157 | // Sort SM groups by init state cref depth so outer SMs are processed first | ||
| 158 | 3 | smGroupPairs := List.zip(initStates, smGroups); | |
| 159 | 3 | smGroupsSorted := List.sort(smGroupPairs, smGroupDepthLt); | |
| 160 | |||
| 161 | // Map from state cref to SM semantics — used to find enclosing SM for nested SMs | ||
| 162 | 3 | stateToSem := UnorderedMap.new<FlatSmSemantics>(ComponentRef.hash, ComponentRef.isEqual); | |
| 163 | |||
| 164 | 3 | smVars := {}; | |
| 165 | smEqs := {}; | ||
| 166 |
2/2✓ Branch 0 taken 3 times.
✓ Branch 1 taken 3 times.
|
6 | for smPair in smGroupsSorted loop |
| 167 | 3 | (initState, stateCrefs) := smPair; | |
| 168 | // Detect hierarchy: if initState has a parent prefix that is a state in another SM | ||
| 169 | 3 | parentPrefix := ComponentRef.rest(initState); | |
| 170 |
1/2✗ Branch 1 not taken.
✓ Branch 2 taken 3 times.
|
3 | if ComponentRef.isEmpty(parentPrefix) then |
| 171 | enclosingStateCrefOpt := NONE(); | ||
| 172 | enclosingSmSemOpt := NONE(); | ||
| 173 | else | ||
| 174 | ✗ | enclosingSmSemOpt := UnorderedMap.get(parentPrefix, stateToSem); | |
| 175 | ✗ | enclosingStateCrefOpt := if isSome(enclosingSmSemOpt) then SOME(parentPrefix) else NONE(); | |
| 176 | end if; | ||
| 177 | |||
| 178 | 3 | (smEqs, smVars, sem) := flatSmToDataFlow( | |
| 179 | initState, | ||
| 180 | stateCrefs, | ||
| 181 | flatModel.equations, | ||
| 182 | flatModel.variables, | ||
| 183 | enclosingStateCrefOpt, enclosingSmSemOpt, | ||
| 184 | smEqs, smVars, | ||
| 185 | outerVarMap); | ||
| 186 | |||
| 187 | // Register all states with their SM semantics for nested SM detection | ||
| 188 |
2/2✓ Branch 0 taken 6 times.
✓ Branch 1 taken 3 times.
|
9 | for sc in stateCrefs loop |
| 189 | 6 | UnorderedMap.addUnique(sc, sem, stateToSem); | |
| 190 | end for; | ||
| 191 | end for; | ||
| 192 | |||
| 193 | // Generate merge equations for outer variables written by state components | ||
| 194 | // e.g.: i = if state1.active then state1.i else if state2.active then state2.i else previous(i) | ||
| 195 |
2/2✓ Branch 1 taken 2 times.
✓ Branch 2 taken 3 times.
|
5 | for outerVarCref in UnorderedMap.keyList(outerVarMap) loop |
| 196 | 2 | (smEqs, smVars) := generateMergeEquation(outerVarCref, outerVarMap, flatModel.variables, smEqs, smVars); | |
| 197 | end for; | ||
| 198 | |||
| 199 | // Substitute activeState(x) → x.active in all equations (SM eqs may contain activeState() from model code) | ||
| 200 |
6/8✓ Branch 0 taken 91 times.
✓ Branch 1 taken 3 times.
✓ Branch 2 taken 91 times.
✓ Branch 3 taken 3 times.
✗ Branch 5 not taken.
✓ Branch 6 taken 3 times.
✗ Branch 7 not taken.
✓ Branch 8 taken 3 times.
|
94 | resultEqs := listAppend(list(subsActiveStateInEq(eq) for eq in smEqs), list(subsActiveStateInEq(eq) for eq in otherEqs)); |
| 201 | 3 | resultVars := listAppend(smVars, flatModel.variables); | |
| 202 | |||
| 203 | 3 | flatModel.equations := resultEqs; | |
| 204 | // Remove initialState() from initialEquations; transition() already removed above | ||
| 205 | flatModel.initialEquations := List.filterOnFalse(flatModel.initialEquations, isTransitionOrInitialState); | ||
| 206 | flatModel.variables := resultVars; | ||
| 207 | |||
| 208 | 3 | execStat(getInstanceName()); | |
| 209 | end flatten; | ||
| 210 | |||
| 211 | // ============================================================ | ||
| 212 | // SM group detection | ||
| 213 | // ============================================================ | ||
| 214 | |||
| 215 | protected | ||
| 216 | function groupStateMachines | ||
| 217 | "Extract flat state machine groups from the equation lists. | ||
| 218 | transition() calls come from equations; initialState() from initialEquations. | ||
| 219 | Returns parallel lists: one initial-state cref per SM group, | ||
| 220 | and one list of all state crefs per SM group." | ||
| 221 | input list<Equation> equations; | ||
| 222 | input list<Equation> initialEquations; | ||
| 223 | output list<ComponentRef> initStates = {}; | ||
| 224 | output list<list<ComponentRef>> smGroups = {}; | ||
| 225 | protected | ||
| 226 | list<ComponentRef> allFroms = {}, allTos = {}, allInits = {}; | ||
| 227 | ComponentRef cr1, cr2; | ||
| 228 | list<ComponentRef> group; | ||
| 229 | algorithm | ||
| 230 | // Collect transition() and initialState() from both equation sections | ||
| 231 |
2/2✓ Branch 1 taken 12 times.
✓ Branch 2 taken 3 times.
|
15 | for eq in listAppend(equations, initialEquations) loop |
| 232 | () := match eq | ||
| 233 | local | ||
| 234 | Call eqCall; | ||
| 235 | String fname; | ||
| 236 | case Equation.NORETCALL(exp = Expression.CALL(call = eqCall)) | ||
| 237 | algorithm | ||
| 238 | 8 | fname := Call.functionNameLast(eqCall); | |
| 239 |
3/4✓ Branch 0 taken 5 times.
✓ Branch 1 taken 3 times.
✓ Branch 3 taken 5 times.
✗ Branch 4 not taken.
|
8 | if stringEq(fname, "transition") then |
| 240 |
5/10✗ Branch 2 not taken.
✓ Branch 3 taken 5 times.
✗ Branch 4 not taken.
✓ Branch 5 taken 5 times.
✗ Branch 6 not taken.
✓ Branch 7 taken 5 times.
✗ Branch 8 not taken.
✓ Branch 9 taken 5 times.
✗ Branch 10 not taken.
✓ Branch 11 taken 5 times.
|
5 | {Expression.CREF(cref = cr1), Expression.CREF(cref = cr2)} := |
| 241 | List.firstN(Call.arguments(eqCall), 2); | ||
| 242 | allFroms := cr1 :: allFroms; | ||
| 243 | 5 | allTos := cr2 :: allTos; | |
| 244 | elseif stringEq(fname, "initialState") then | ||
| 245 |
3/6✗ Branch 2 not taken.
✓ Branch 3 taken 3 times.
✗ Branch 4 not taken.
✓ Branch 5 taken 3 times.
✗ Branch 6 not taken.
✓ Branch 7 taken 3 times.
|
3 | {Expression.CREF(cref = cr1)} := List.firstN(Call.arguments(eqCall), 1); |
| 246 | allInits := cr1 :: allInits; | ||
| 247 | end if; | ||
| 248 | then (); | ||
| 249 | else (); | ||
| 250 | end match; | ||
| 251 | end for; | ||
| 252 | |||
| 253 | // Group states by connectivity (each initialState defines one flat SM) | ||
| 254 | // Simple approach: each initialState is the root of one flat SM, | ||
| 255 | // containing all states reachable via transitions | ||
| 256 |
2/2✓ Branch 0 taken 3 times.
✓ Branch 1 taken 3 times.
|
6 | for initCref in allInits loop |
| 257 | 3 | group := collectReachableStates(initCref, allFroms, allTos); | |
| 258 | initStates := initCref :: initStates; | ||
| 259 | smGroups := group :: smGroups; | ||
| 260 | end for; | ||
| 261 | |||
| 262 | 3 | initStates := listReverse(initStates); | |
| 263 | 3 | smGroups := listReverse(smGroups); | |
| 264 | end groupStateMachines; | ||
| 265 | |||
| 266 | protected | ||
| 267 | function collectReachableStates | ||
| 268 | "Collect all states reachable from initCref via transitions (BFS)." | ||
| 269 | input ComponentRef initCref; | ||
| 270 | input list<ComponentRef> froms; | ||
| 271 | input list<ComponentRef> tos; | ||
| 272 | output list<ComponentRef> states; | ||
| 273 | protected | ||
| 274 | list<ComponentRef> queue = {initCref}; | ||
| 275 | list<ComponentRef> visited = {}; | ||
| 276 | ComponentRef cur; | ||
| 277 | algorithm | ||
| 278 | states := {}; | ||
| 279 |
2/2✓ Branch 0 taken 13 times.
✓ Branch 1 taken 3 times.
|
16 | while not listEmpty(queue) loop |
| 280 | 13 | cur :: queue := queue; | |
| 281 |
2/2✓ Branch 1 taken 7 times.
✓ Branch 2 taken 6 times.
|
13 | if not List.isMemberOnTrue(cur, visited, ComponentRef.isEqual) then |
| 282 | visited := cur :: visited; | ||
| 283 | states := cur :: states; | ||
| 284 | // Find neighbors | ||
| 285 |
1/2✗ Branch 1 not taken.
✓ Branch 2 taken 6 times.
|
16 | for i in 1:listLength(froms) loop |
| 286 |
2/2✓ Branch 2 taken 5 times.
✓ Branch 3 taken 5 times.
|
10 | if ComponentRef.isEqual(listGet(froms, i), cur) then |
| 287 | 5 | queue := listGet(tos, i) :: queue; | |
| 288 | end if; | ||
| 289 |
2/2✓ Branch 2 taken 5 times.
✓ Branch 3 taken 5 times.
|
10 | if ComponentRef.isEqual(listGet(tos, i), cur) then |
| 290 | 5 | queue := listGet(froms, i) :: queue; | |
| 291 | end if; | ||
| 292 | end for; | ||
| 293 | end if; | ||
| 294 | end while; | ||
| 295 | // Put initial state first. | ||
| 296 | // List.sort uses "greater-than" semantics: compare(a,b)=true means b comes before a. | ||
| 297 | 3 | states := List.sort(states, function statePriorityGt(initCref = initCref)); | |
| 298 | end collectReachableStates; | ||
| 299 | |||
| 300 | protected | ||
| 301 | function statePriorityGt | ||
| 302 | "Sort comparator (greater-than semantics for List.sort) so initCref comes first." | ||
| 303 | input ComponentRef cr1; | ||
| 304 | input ComponentRef cr2; | ||
| 305 | input ComponentRef initCref; | ||
| 306 | output Boolean gt; | ||
| 307 | algorithm | ||
| 308 | // compare(a, b) = true → b should come before a | ||
| 309 |
1/2✓ Branch 1 taken 3 times.
✗ Branch 2 not taken.
|
3 | if ComponentRef.isEqual(cr2, initCref) then |
| 310 | gt := true; // cr2 is the init state → cr2 should come first → cr1 > cr2 | ||
| 311 | elseif ComponentRef.isEqual(cr1, initCref) then | ||
| 312 | gt := false; // cr1 is the init state → cr1 should come first → cr1 < cr2 (NOT greater) | ||
| 313 | else | ||
| 314 | ✗ | gt := ComponentRef.toString(cr1) > ComponentRef.toString(cr2); | |
| 315 | end if; | ||
| 316 | end statePriorityGt; | ||
| 317 | |||
| 318 | // ============================================================ | ||
| 319 | // Flat SM to data-flow transformation | ||
| 320 | // ============================================================ | ||
| 321 | |||
| 322 | protected | ||
| 323 | function smGroupDepthLt | ||
| 324 | "Comparator for sorting SM groups by cref depth (outer SMs first)." | ||
| 325 | input tuple<ComponentRef, list<ComponentRef>> g1; | ||
| 326 | input tuple<ComponentRef, list<ComponentRef>> g2; | ||
| 327 | output Boolean lt; | ||
| 328 | protected | ||
| 329 | ComponentRef c1, c2; | ||
| 330 | algorithm | ||
| 331 | ✗ | (c1, _) := g1; | |
| 332 | ✗ | (c2, _) := g2; | |
| 333 | ✗ | lt := ComponentRef.depth(c1) < ComponentRef.depth(c2); | |
| 334 | end smGroupDepthLt; | ||
| 335 | |||
| 336 | protected | ||
| 337 | function flatSmToDataFlow | ||
| 338 | "Transform one flat state machine into data-flow equations and variables." | ||
| 339 | input ComponentRef initStateCref; | ||
| 340 | input list<ComponentRef> stateCrefs "All state crefs, init state first"; | ||
| 341 | input list<Equation> allEquations; | ||
| 342 | input list<Variable> allVariables; | ||
| 343 | input Option<ComponentRef> enclosingStateCrefOpt; | ||
| 344 | input Option<FlatSmSemantics> enclosingSmSemOpt; | ||
| 345 | input output list<Equation> accEqs; | ||
| 346 | input output list<Variable> accVars; | ||
| 347 | input UnorderedMap<ComponentRef, list<tuple<ComponentRef, ComponentRef>>> outerVarMap; | ||
| 348 | output FlatSmSemantics outSem; | ||
| 349 | protected | ||
| 350 | list<Equation> transitionEqs, initialStateEqs; | ||
| 351 | FlatSmSemantics sem, semWithProp, semFinal; | ||
| 352 | ComponentRef parentPrefix; | ||
| 353 | list<String> varCrefStrings; | ||
| 354 | algorithm | ||
| 355 | // Extract transition and initialState equations for this SM group | ||
| 356 | 3 | transitionEqs := List.filterOnTrue(allEquations, | |
| 357 | function isTransitionForGroup(stateCrefs = stateCrefs)); | ||
| 358 | 3 | initialStateEqs := List.filterOnTrue(allEquations, | |
| 359 | function isInitialStateForGroup(initStateCref = initStateCref)); | ||
| 360 | |||
| 361 | // Build basic semantics | ||
| 362 | 3 | sem := basicFlatSmSemantics(initStateCref, stateCrefs, transitionEqs); | |
| 363 | |||
| 364 | // Add propagation equations | ||
| 365 | 3 | semWithProp := addPropagationEquations(sem, enclosingStateCrefOpt, enclosingSmSemOpt); | |
| 366 | |||
| 367 | // Elaborate ticksInState/timeInState operators | ||
| 368 | 3 | semFinal := elabXInStateOps(semWithProp, enclosingStateCrefOpt); | |
| 369 | |||
| 370 | // Fix inner/outer variable references in transition conditions. | ||
| 371 | // NF resolves 'inner outer y' to the outermost scope variable, but nested SM | ||
| 372 | // transition conditions need the intermediate-scope version (e.g., 'a.y' not 'y'). | ||
| 373 | 3 | parentPrefix := ComponentRef.rest(listHead(stateCrefs)); | |
| 374 |
1/2✗ Branch 1 not taken.
✓ Branch 2 taken 3 times.
|
3 | if not ComponentRef.isEmpty(parentPrefix) then |
| 375 | ✗ | varCrefStrings := list(ComponentRef.toString(v.name) for v in allVariables); | |
| 376 | ✗ | semFinal.eqs := List.map(semFinal.eqs, | |
| 377 | function Equation.mapExp(func = function qualifyOuterVarExpr(parentPrefix = parentPrefix, varCrefStrings = varCrefStrings))); | ||
| 378 | end if; | ||
| 379 | |||
| 380 | // Accumulate SMS variables and equations | ||
| 381 | 3 | accVars := List.flatten({accVars, semFinal.vars, semFinal.knowns, semFinal.pvars}); | |
| 382 | 6 | accEqs := List.flatten({accEqs, semFinal.eqs, semFinal.peqs}); | |
| 383 | |||
| 384 | // Transform state component equations | ||
| 385 |
2/2✓ Branch 0 taken 6 times.
✓ Branch 1 taken 3 times.
|
9 | for stateCref in stateCrefs loop |
| 386 | 6 | (accEqs, accVars) := smCompToDataFlow(stateCref, semFinal, allEquations, allVariables, accEqs, accVars, outerVarMap); | |
| 387 | end for; | ||
| 388 | |||
| 389 | outSem := semFinal; | ||
| 390 | end flatSmToDataFlow; | ||
| 391 | |||
| 392 | protected | ||
| 393 | function qualifyOuterVarExpr | ||
| 394 | "Applied via Equation.mapExp: recursively qualifies bare crefs in an expression." | ||
| 395 | input output Expression e; | ||
| 396 | input ComponentRef parentPrefix; | ||
| 397 | input list<String> varCrefStrings; | ||
| 398 | algorithm | ||
| 399 | ✗ | e := Expression.map(e, function qualifyOuterVarCref(parentPrefix = parentPrefix, varCrefStrings = varCrefStrings)); | |
| 400 | end qualifyOuterVarExpr; | ||
| 401 | |||
| 402 | protected | ||
| 403 | function qualifyOuterVarCref | ||
| 404 | "Replace a bare cref 'v' with 'parentPrefix.v' if 'parentPrefix.v' is a flat model variable. | ||
| 405 | Fixes NF inner/outer resolution in transition conditions of nested state machines." | ||
| 406 | input output Expression e; | ||
| 407 | input ComponentRef parentPrefix; | ||
| 408 | input list<String> varCrefStrings; | ||
| 409 | protected | ||
| 410 | ComponentRef qualCref; | ||
| 411 | algorithm | ||
| 412 | () := match e | ||
| 413 | case Expression.CREF() | ||
| 414 | guard ComponentRef.isSimple(e.cref) | ||
| 415 | algorithm | ||
| 416 | ✗ | qualCref := ComponentRef.append(e.cref, parentPrefix); | |
| 417 | ✗ | if listMember(ComponentRef.toString(qualCref), varCrefStrings) then | |
| 418 | ✗ | e := Expression.CREF(e.ty, qualCref); | |
| 419 | end if; | ||
| 420 | then (); | ||
| 421 | else (); | ||
| 422 | end match; | ||
| 423 | end qualifyOuterVarCref; | ||
| 424 | |||
| 425 | // ============================================================ | ||
| 426 | // State machine component to data-flow | ||
| 427 | // ============================================================ | ||
| 428 | |||
| 429 | protected | ||
| 430 | function smCompToDataFlow | ||
| 431 | "Transform equations belonging to a state component into conditional data-flow equations." | ||
| 432 | input ComponentRef stateCref; | ||
| 433 | input FlatSmSemantics sem; | ||
| 434 | input list<Equation> allEquations; | ||
| 435 | input list<Variable> allVariables; | ||
| 436 | input output list<Equation> accEqs; | ||
| 437 | input output list<Variable> accVars; | ||
| 438 | input UnorderedMap<ComponentRef, list<tuple<ComponentRef, ComponentRef>>> outerVarMap; | ||
| 439 | protected | ||
| 440 | list<Equation> stateEqs; | ||
| 441 | list<Variable> stateVars; | ||
| 442 | UnorderedMap<ComponentRef, Expression> crToStart; | ||
| 443 | list<Equation> transformedEqs; | ||
| 444 | list<Variable> extraVars; | ||
| 445 | algorithm | ||
| 446 | // Equations belonging to this state (by LHS prefix or by instantiation scope) | ||
| 447 | 6 | stateEqs := List.filterOnTrue(allEquations, | |
| 448 | function isEquationOfState(stateCref = stateCref)); | ||
| 449 | |||
| 450 | // Variables belonging to this state (by cref prefix) | ||
| 451 | 6 | stateVars := List.filterOnTrue(allVariables, | |
| 452 | function isVariableOfState(stateCref = stateCref)); | ||
| 453 | |||
| 454 | // Build map: stateVar cref → start value, but only for variables where | ||
| 455 | // previous(x) appears in an equation (matches old StateMachineFlatten behavior). | ||
| 456 | // Variables without previous(x) in equations use plain previous(x) in the else branch. | ||
| 457 | 6 | crToStart := UnorderedMap.new<Expression>(ComponentRef.hash, ComponentRef.isEqual); | |
| 458 |
1/2✗ Branch 0 not taken.
✓ Branch 1 taken 6 times.
|
6 | for v in stateVars loop |
| 459 | ✗ | if List.any(stateEqs, function equationHasPrevious(varCref = v.name)) then | |
| 460 | ✗ | UnorderedMap.addUnique(v.name, getStartValue(v), crToStart); | |
| 461 | end if; | ||
| 462 | end for; | ||
| 463 | |||
| 464 | // Transform each equation | ||
| 465 | transformedEqs := {}; | ||
| 466 | 6 | extraVars := {}; | |
| 467 |
2/2✓ Branch 0 taken 4 times.
✓ Branch 1 taken 6 times.
|
10 | for eq in stateEqs loop |
| 468 | 4 | (transformedEqs, extraVars) := addStateActivationAndReset(eq, stateCref, sem, crToStart, transformedEqs, extraVars, outerVarMap); | |
| 469 | end for; | ||
| 470 | |||
| 471 | 6 | accEqs := listAppend(listReverse(transformedEqs), accEqs); | |
| 472 | 6 | accVars := listAppend(listReverse(extraVars), accVars); | |
| 473 | |||
| 474 | // For hierarchical states: add outerVarMap entries for inner-outer variables. | ||
| 475 | // E.g., state 'a' with 'inner outer output y' → a.y exists in flat model. | ||
| 476 | // The inner SM merge already gives 'a.y = ...'; we need 'y = if a.active then a.y else previous(y)'. | ||
| 477 | 6 | addHierarchicalPassThroughs(stateCref, sem, allVariables, outerVarMap); | |
| 478 | end smCompToDataFlow; | ||
| 479 | |||
| 480 | protected | ||
| 481 | function addHierarchicalPassThroughs | ||
| 482 | "For a hierarchical state s (one that has inner state machines), generate | ||
| 483 | outerVarMap entries for inner-outer variables: s.v → (s.active, s.v). | ||
| 484 | This causes generateMergeEquation to emit: v = if s.active then s.v else previous(v). | ||
| 485 | Only adds entries when v is a top-level flat variable and not already in outerVarMap." | ||
| 486 | input ComponentRef stateCref; | ||
| 487 | input FlatSmSemantics sem; | ||
| 488 | input list<Variable> allVariables; | ||
| 489 | input UnorderedMap<ComponentRef, list<tuple<ComponentRef, ComponentRef>>> outerVarMap; | ||
| 490 | protected | ||
| 491 | String stateStr, leafName; | ||
| 492 | ComponentRef activeRef, topVarCref; | ||
| 493 | Variable topVar; | ||
| 494 | algorithm | ||
| 495 | 6 | stateStr := ComponentRef.toString(stateCref); | |
| 496 | 6 | activeRef := qCref("active", Type.BOOLEAN(), {}, stateCref); | |
| 497 | |||
| 498 |
2/2✓ Branch 0 taken 4 times.
✓ Branch 1 taken 6 times.
|
10 | for v in allVariables loop |
| 499 | // Check if v is a direct child of stateCref (rest(v.name) == stateCref) | ||
| 500 |
1/6✗ Branch 1 not taken.
✓ Branch 2 taken 4 times.
✗ Branch 5 not taken.
✗ Branch 6 not taken.
✗ Branch 10 not taken.
✗ Branch 11 not taken.
|
4 | if not ComponentRef.isSimple(v.name) and |
| 501 | stringEqual(ComponentRef.toString(ComponentRef.rest(v.name)), stateStr) then | ||
| 502 | ✗ | leafName := ComponentRef.firstName(v.name); | |
| 503 | // Find the top-level (bare) variable with the same leaf name | ||
| 504 | try | ||
| 505 | ✗ | topVar := List.find(allVariables, | |
| 506 | function isSimpleVarNamed(name = leafName)); | ||
| 507 | ✗ | topVarCref := topVar.name; | |
| 508 | // Only add if not already in outerVarMap (direct outer-output already added it) | ||
| 509 | ✗ | if not UnorderedMap.contains(topVarCref, outerVarMap) then | |
| 510 | ✗ | UnorderedMap.add(topVarCref, {(activeRef, v.name)}, outerVarMap); | |
| 511 | end if; | ||
| 512 | else | ||
| 513 | // No top-level variable found — not an inner-outer variable, skip | ||
| 514 | end try; | ||
| 515 | end if; | ||
| 516 | end for; | ||
| 517 | end addHierarchicalPassThroughs; | ||
| 518 | |||
| 519 | protected | ||
| 520 | function isSimpleVarNamed | ||
| 521 | "True if the variable has a bare cref (no prefix) with the given leaf name." | ||
| 522 | input Variable v; | ||
| 523 | input String name; | ||
| 524 | output Boolean res; | ||
| 525 | algorithm | ||
| 526 | ✗ | res := ComponentRef.isSimple(v.name) and stringEqual(ComponentRef.firstName(v.name), name); | |
| 527 | end isSimpleVarNamed; | ||
| 528 | |||
| 529 | // ============================================================ | ||
| 530 | // addStateActivationAndReset | ||
| 531 | // ============================================================ | ||
| 532 | |||
| 533 | protected | ||
| 534 | function addStateActivationAndReset | ||
| 535 | "Make equations conditional on state activation; add reset equations for state variables." | ||
| 536 | input Equation inEq; | ||
| 537 | input ComponentRef stateCref; | ||
| 538 | input FlatSmSemantics sem; | ||
| 539 | input UnorderedMap<ComponentRef, Expression> crToStart; | ||
| 540 | input output list<Equation> accEqs; | ||
| 541 | input output list<Variable> accVars; | ||
| 542 | input UnorderedMap<ComponentRef, list<tuple<ComponentRef, ComponentRef>>> outerVarMap; | ||
| 543 | algorithm | ||
| 544 | () := match inEq | ||
| 545 | case Equation.EQUALITY() | ||
| 546 | algorithm | ||
| 547 | 4 | (accEqs, accVars) := addStateActivationAndReset1(inEq, stateCref, sem, crToStart, accEqs, accVars, outerVarMap); | |
| 548 | then (); | ||
| 549 | |||
| 550 | case Equation.WHEN() | ||
| 551 | algorithm | ||
| 552 | // Recursively transform equations in WHEN branches; propagate generated vars | ||
| 553 | ✗ | (accEqs, accVars) := transformWhenBranchesAndAccumulate(inEq, stateCref, sem, crToStart, outerVarMap, accEqs, accVars); | |
| 554 | then (); | ||
| 555 | |||
| 556 | else | ||
| 557 | algorithm | ||
| 558 | accEqs := inEq :: accEqs; | ||
| 559 | then (); | ||
| 560 | end match; | ||
| 561 | end addStateActivationAndReset; | ||
| 562 | |||
| 563 | protected | ||
| 564 | function transformWhenBranchesAndAccumulate | ||
| 565 | "Transforms WHEN equation equations belonging to a state. | ||
| 566 | For clocked when (Clock condition): extracts inner equations as plain equations | ||
| 567 | to match old StateMachineFlatten behavior (backend detects clocked partition via previous()). | ||
| 568 | For event when (Boolean condition): keeps WHEN wrapper." | ||
| 569 | input Equation whenEq; | ||
| 570 | input ComponentRef stateCref; | ||
| 571 | input FlatSmSemantics sem; | ||
| 572 | input UnorderedMap<ComponentRef, Expression> crToStart; | ||
| 573 | input UnorderedMap<ComponentRef, list<tuple<ComponentRef, ComponentRef>>> outerVarMap; | ||
| 574 | input output list<Equation> accEqs; | ||
| 575 | input output list<Variable> accVars; | ||
| 576 | protected | ||
| 577 | list<Equation.Branch> branches; | ||
| 578 | Equation.Branch firstBranch; | ||
| 579 | Expression branchCond; | ||
| 580 | Equation outEq; | ||
| 581 | list<Variable> extraVars; | ||
| 582 | list<Equation> innerEqs; | ||
| 583 | list<Variable> innerVars; | ||
| 584 | algorithm | ||
| 585 | ✗ | Equation.WHEN(branches = branches) := whenEq; | |
| 586 | ✗ | firstBranch := listHead(branches); | |
| 587 | ✗ | Equation.Branch.BRANCH(condition = branchCond) := firstBranch; | |
| 588 | ✗ | if Type.isClock(Expression.typeOf(branchCond)) then | |
| 589 | // Clocked when: extract inner equations as plain equations | ||
| 590 | ✗ | (innerEqs, innerVars) := transformWhenInnerAsPlain(whenEq, stateCref, sem, crToStart, outerVarMap); | |
| 591 | ✗ | accEqs := listAppend(innerEqs, accEqs); | |
| 592 | ✗ | accVars := listAppend(innerVars, accVars); | |
| 593 | else | ||
| 594 | // Event when: keep WHEN wrapper | ||
| 595 | ✗ | (outEq, extraVars) := transformWhenBranches(whenEq, stateCref, sem, crToStart, outerVarMap); | |
| 596 | accEqs := outEq :: accEqs; | ||
| 597 | ✗ | accVars := listAppend(extraVars, accVars); | |
| 598 | end if; | ||
| 599 | end transformWhenBranchesAndAccumulate; | ||
| 600 | |||
| 601 | protected | ||
| 602 | function transformWhenInnerAsPlain | ||
| 603 | "For a clocked when equation, extract and transform inner equations as plain equations." | ||
| 604 | input Equation whenEq; | ||
| 605 | input ComponentRef stateCref; | ||
| 606 | input FlatSmSemantics sem; | ||
| 607 | input UnorderedMap<ComponentRef, Expression> crToStart; | ||
| 608 | input UnorderedMap<ComponentRef, list<tuple<ComponentRef, ComponentRef>>> outerVarMap; | ||
| 609 | output list<Equation> outEqs = {}; | ||
| 610 | output list<Variable> outVars = {}; | ||
| 611 | protected | ||
| 612 | list<Equation.Branch> branches; | ||
| 613 | list<Equation> branchBody, transformedBody; | ||
| 614 | list<Variable> branchVars; | ||
| 615 | algorithm | ||
| 616 | ✗ | Equation.WHEN(branches = branches) := whenEq; | |
| 617 | ✗ | for branch in branches loop | |
| 618 | () := match branch | ||
| 619 | case Equation.Branch.BRANCH(body = branchBody) | ||
| 620 | algorithm | ||
| 621 | transformedBody := {}; | ||
| 622 | ✗ | branchVars := {}; | |
| 623 | ✗ | for eq in branchBody loop | |
| 624 | ✗ | (transformedBody, branchVars) := addStateActivationAndReset(eq, stateCref, sem, crToStart, transformedBody, branchVars, outerVarMap); | |
| 625 | end for; | ||
| 626 | ✗ | outEqs := listAppend(listReverse(transformedBody), outEqs); | |
| 627 | ✗ | outVars := listAppend(branchVars, outVars); | |
| 628 | then (); | ||
| 629 | else (); | ||
| 630 | end match; | ||
| 631 | end for; | ||
| 632 | end transformWhenInnerAsPlain; | ||
| 633 | |||
| 634 | protected | ||
| 635 | function transformWhenBranches | ||
| 636 | input Equation whenEq; | ||
| 637 | input ComponentRef stateCref; | ||
| 638 | input FlatSmSemantics sem; | ||
| 639 | input UnorderedMap<ComponentRef, Expression> crToStart; | ||
| 640 | input UnorderedMap<ComponentRef, list<tuple<ComponentRef, ComponentRef>>> outerVarMap; | ||
| 641 | output Equation outEq; | ||
| 642 | output list<Variable> extraVars = {}; | ||
| 643 | protected | ||
| 644 | list<Equation.Branch> branches, newBranches; | ||
| 645 | list<Equation> transformedBody; | ||
| 646 | list<Variable> branchVars; | ||
| 647 | NFInstNode.ScopeRef whenScope; | ||
| 648 | DAE.ElementSource whenSource; | ||
| 649 | Expression branchCond; | ||
| 650 | Variability branchCondVar; | ||
| 651 | list<Equation> branchBody; | ||
| 652 | algorithm | ||
| 653 | ✗ | Equation.WHEN(branches = branches, scope = whenScope, source = whenSource) := whenEq; | |
| 654 | newBranches := {}; | ||
| 655 | ✗ | for branch in branches loop | |
| 656 | branch := match branch | ||
| 657 | case Equation.Branch.BRANCH(condition = branchCond, conditionVar = branchCondVar, body = branchBody) | ||
| 658 | algorithm | ||
| 659 | transformedBody := {}; | ||
| 660 | ✗ | branchVars := {}; | |
| 661 | ✗ | for eq in branchBody loop | |
| 662 | ✗ | (transformedBody, branchVars) := addStateActivationAndReset(eq, stateCref, sem, crToStart, transformedBody, branchVars, outerVarMap); | |
| 663 | end for; | ||
| 664 | ✗ | extraVars := listAppend(branchVars, extraVars); | |
| 665 | ✗ | then Equation.Branch.BRANCH(branchCond, branchCondVar, listReverse(transformedBody)); | |
| 666 | else branch; | ||
| 667 | end match; | ||
| 668 | newBranches := branch :: newBranches; | ||
| 669 | end for; | ||
| 670 | ✗ | outEq := Equation.WHEN(listReverse(newBranches), whenScope, whenSource); | |
| 671 | end transformWhenBranches; | ||
| 672 | |||
| 673 | protected | ||
| 674 | function addStateActivationAndReset1 | ||
| 675 | "Transform a simple equation: make conditional on state.active; add reset for state variables. | ||
| 676 | For outer-output equations (LHS is not state-prefixed but scope is state): create per-state variable." | ||
| 677 | input Equation inEq; | ||
| 678 | input ComponentRef stateCref; | ||
| 679 | input FlatSmSemantics sem; | ||
| 680 | input UnorderedMap<ComponentRef, Expression> crToStart; | ||
| 681 | input output list<Equation> accEqs; | ||
| 682 | input output list<Variable> accVars; | ||
| 683 | input UnorderedMap<ComponentRef, list<tuple<ComponentRef, ComponentRef>>> outerVarMap; | ||
| 684 | protected | ||
| 685 | Expression lhs, rhs; | ||
| 686 | ComponentRef lhsCref, perStateVarCref, stateActiveCref; | ||
| 687 | Type lhsTy; | ||
| 688 | NFInstNode.ScopeRef eqScope; | ||
| 689 | DAE.ElementSource eqSource; | ||
| 690 | list<ComponentRef> stateVarCrefs; | ||
| 691 | Boolean hasStateVarOnLHS, isOuterOutput; | ||
| 692 | Expression newRhs, perStateVarExp; | ||
| 693 | Equation eq1, eq2; | ||
| 694 | Variable perStateVar; | ||
| 695 | list<tuple<ComponentRef, ComponentRef>> prevList; | ||
| 696 | algorithm | ||
| 697 |
1/2✗ Branch 0 not taken.
✓ Branch 1 taken 4 times.
|
4 | Equation.EQUALITY(lhs = lhs, rhs = rhs, ty = lhsTy, scope = eqScope, source = eqSource) := inEq; |
| 698 | 4 | stateVarCrefs := UnorderedMap.keyList(crToStart); | |
| 699 | |||
| 700 | try | ||
| 701 |
1/2✗ Branch 0 not taken.
✓ Branch 1 taken 4 times.
|
4 | Expression.CREF(ty = lhsTy, cref = lhsCref) := lhs; |
| 702 | |||
| 703 | // Substitute previous(x) → x_previous for state variables in RHS | ||
| 704 | 4 | (newRhs, _) := Expression.mapFold(rhs, | |
| 705 | function subsPreviousCrefs(stateVarCrefs = stateVarCrefs), false); | ||
| 706 | 4 | eq1 := Equation.EQUALITY(lhs, newRhs, lhsTy, eqScope, eqSource, ScalarizeMode.NO_PREFERENCE); | |
| 707 | |||
| 708 | // Check if this is an outer-output equation: | ||
| 709 | // LHS is NOT state-prefixed but the equation's scope is the state component | ||
| 710 |
3/6✓ Branch 1 taken 4 times.
✗ Branch 2 not taken.
✓ Branch 6 taken 4 times.
✗ Branch 7 not taken.
✓ Branch 12 taken 4 times.
✗ Branch 13 not taken.
|
4 | isOuterOutput := not crefHasPrefix(stateCref, lhsCref) and |
| 711 | stringEqual(InstNode.name(InstNode.fromCell(eqScope)), ComponentRef.firstName(stateCref)); | ||
| 712 | |||
| 713 | if isOuterOutput then | ||
| 714 | // Outer output: x = rhs from state1 → create state1.x per-state variable | ||
| 715 | // Generate: state1.x = if state1.active then rhs else previous(state1.x) | ||
| 716 | // Track in outerVarMap for merge equation generation | ||
| 717 | 4 | perStateVarCref := ComponentRef.prefixCref( | |
| 718 | InstNode.NAME_NODE(ComponentRef.firstName(lhsCref)), lhsTy, {}, stateCref); | ||
| 719 | 4 | perStateVar := makeVarWithStart(perStateVarCref, lhsTy, Variability.DISCRETE, | |
| 720 | getDefaultStart(lhsTy)); | ||
| 721 | 4 | perStateVarExp := makeCrefExp(perStateVarCref, lhsTy); | |
| 722 | // state1.x = if state1.active then rhs else previous(state1.x) | ||
| 723 | 4 | eq1 := Equation.EQUALITY(perStateVarExp, newRhs, lhsTy, eqScope, eqSource, ScalarizeMode.NO_PREFERENCE); | |
| 724 | 4 | eq1 := wrapInStateActivationConditional(eq1, stateCref, false); | |
| 725 | 4 | accEqs := eq1 :: accEqs; | |
| 726 | 4 | accVars := perStateVar :: accVars; | |
| 727 | // Record in outerVarMap: outerVar → (stateActiveCref, perStateVarCref) | ||
| 728 | 4 | stateActiveCref := qCref("active", Type.BOOLEAN(), {}, stateCref); | |
| 729 | 4 | prevList := UnorderedMap.getOrDefault(lhsCref, outerVarMap, {}); | |
| 730 | 8 | UnorderedMap.add(lhsCref, (stateActiveCref, perStateVarCref) :: prevList, outerVarMap); | |
| 731 | |||
| 732 | else | ||
| 733 | // Check if LHS is a state variable (one that has previous(x) applied to it) | ||
| 734 | hasStateVarOnLHS := false; | ||
| 735 | ✗ | for svc in stateVarCrefs loop | |
| 736 | ✗ | hasStateVarOnLHS := ComponentRef.isEqual(svc, lhsCref); | |
| 737 | ✗ | if hasStateVarOnLHS then | |
| 738 | break; | ||
| 739 | end if; | ||
| 740 | end for; | ||
| 741 | ✗ | if hasStateVarOnLHS then | |
| 742 | // Transform: x = e → x = if active then e else x_previous | ||
| 743 | ✗ | eq1 := wrapInStateActivationConditional(eq1, stateCref, true); | |
| 744 | // Add reset equation: x_previous = if active and (reset or activeResetStates[i]) then x_start else previous(x) | ||
| 745 | ✗ | eq2 := createResetEquation(lhsCref, lhsTy, stateCref, sem, crToStart); | |
| 746 | // Add fresh variable x_previous | ||
| 747 | ✗ | accEqs := eq1 :: eq2 :: accEqs; | |
| 748 | ✗ | accVars := makeVar( | |
| 749 | ComponentRef.prefixCref(InstNode.NAME_NODE(ComponentRef.firstName(lhsCref) + "_previous"), | ||
| 750 | lhsTy, {}, ComponentRef.rest(lhsCref)), | ||
| 751 | lhsTy, Variability.CONTINUOUS) :: accVars; | ||
| 752 | else | ||
| 753 | // Not a state variable: just wrap with activation condition | ||
| 754 | ✗ | accEqs := wrapInStateActivationConditional(eq1, stateCref, false) :: accEqs; | |
| 755 | end if; | ||
| 756 | end if; | ||
| 757 | else | ||
| 758 | // Fallback: pass equation through unchanged | ||
| 759 | accEqs := inEq :: accEqs; | ||
| 760 | end try; | ||
| 761 | end addStateActivationAndReset1; | ||
| 762 | |||
| 763 | protected | ||
| 764 | function equationHasPrevious | ||
| 765 | "True if previous(varCref) appears anywhere in the equation's expressions." | ||
| 766 | input Equation eq; | ||
| 767 | input ComponentRef varCref; | ||
| 768 | output Boolean found; | ||
| 769 | algorithm | ||
| 770 | ✗ | found := Equation.containsExp(eq, | |
| 771 | function Expression.contains(func = function isPreviousOfCref(varCref = varCref))); | ||
| 772 | end equationHasPrevious; | ||
| 773 | |||
| 774 | protected | ||
| 775 | function isPreviousOfCref | ||
| 776 | "True if e is previous(varCref)." | ||
| 777 | input Expression e; | ||
| 778 | input ComponentRef varCref; | ||
| 779 | output Boolean res; | ||
| 780 | protected | ||
| 781 | Call expCall; | ||
| 782 | list<Expression> args; | ||
| 783 | ComponentRef argCref; | ||
| 784 | algorithm | ||
| 785 | res := match e | ||
| 786 | case Expression.CALL(call = expCall) | ||
| 787 | guard stringEq(Call.functionNameLast(expCall), "previous") | ||
| 788 | algorithm | ||
| 789 | ✗ | args := Call.arguments(expCall); | |
| 790 | res := false; | ||
| 791 | ✗ | if listLength(args) == 1 then | |
| 792 | res := match listHead(args) | ||
| 793 | ✗ | case Expression.CREF(cref = argCref) then ComponentRef.isEqual(argCref, varCref); | |
| 794 | else false; | ||
| 795 | end match; | ||
| 796 | end if; | ||
| 797 | then res; | ||
| 798 | else false; | ||
| 799 | end match; | ||
| 800 | end isPreviousOfCref; | ||
| 801 | |||
| 802 | protected | ||
| 803 | function getDefaultStart | ||
| 804 | "Get a default start value for a given type." | ||
| 805 | input Type ty; | ||
| 806 | output Expression result; | ||
| 807 | algorithm | ||
| 808 | result := match ty | ||
| 809 | case Type.INTEGER() then Expression.INTEGER(0); | ||
| 810 | case Type.REAL() then Expression.REAL(0.0); | ||
| 811 | case Type.BOOLEAN() then Expression.BOOLEAN(false); | ||
| 812 | case Type.STRING() then Expression.STRING(""); | ||
| 813 | else Expression.INTEGER(0); | ||
| 814 | end match; | ||
| 815 | end getDefaultStart; | ||
| 816 | |||
| 817 | // ============================================================ | ||
| 818 | // basicFlatSmSemantics | ||
| 819 | // ============================================================ | ||
| 820 | |||
| 821 | protected | ||
| 822 | function basicFlatSmSemantics | ||
| 823 | "Create variables and equations implementing MLS §17.3.4 state machine semantics." | ||
| 824 | input ComponentRef initStateCref; | ||
| 825 | input list<ComponentRef> stateCrefs "All states; index 1 = initial state"; | ||
| 826 | input list<Equation> transitionEqs; | ||
| 827 | output FlatSmSemantics sem; | ||
| 828 | protected | ||
| 829 | ComponentRef preRef; | ||
| 830 | Integer nStates, nTransitions, i; | ||
| 831 | list<Transition> t; | ||
| 832 | list<Expression> cExps; | ||
| 833 | list<Variable> vars = {}, knowns = {}; | ||
| 834 | list<Equation> eqs = {}; | ||
| 835 | |||
| 836 | // Scalar references for semantic variables | ||
| 837 | ComponentRef nStatesRef, activeRef, resetRef, selectedStateRef, selectedResetRef, | ||
| 838 | firedRef, activeStateRef, activeResetRef, nextStateRef, nextResetRef, | ||
| 839 | stateMachineInFinalStateRef; | ||
| 840 | |||
| 841 | // Array references (sized by nStates) | ||
| 842 | Type tArrayBool, tArrayInt; | ||
| 843 | list<ComponentRef> activeResetStatesRefs = {}, nextResetStatesRefs = {}, finalStatesRefs = {}; | ||
| 844 | list<ComponentRef> cRefs = {}, cImmediateRefs = {}; | ||
| 845 | |||
| 846 | // Array references (sized by nTransitions) | ||
| 847 | Type tTArrayBool, tTArrayInt; | ||
| 848 | list<ComponentRef> tFromRefs = {}, tToRefs = {}, tImmediateRefs = {}, tResetRefs = {}, | ||
| 849 | tSynchronizeRefs = {}, tPriorityRefs = {}; | ||
| 850 | |||
| 851 | Expression rhs, expCond, expThen, expElse, exp1, exp2, expIf; | ||
| 852 | list<Expression> expLst; | ||
| 853 | Boolean immediateVal; | ||
| 854 | |||
| 855 | // Dimension objects | ||
| 856 | Dimension tDim, nStatesDim; | ||
| 857 | algorithm | ||
| 858 | 3 | preRef := makeSMSPrefix(initStateCref); | |
| 859 | 3 | (t, cExps) := createTandC(stateCrefs, transitionEqs); | |
| 860 | |||
| 861 | 3 | nStates := listLength(stateCrefs); | |
| 862 | 3 | nTransitions := listLength(t); | |
| 863 | 3 | tDim := Dimension.INTEGER(nTransitions, Variability.STRUCTURAL_PARAMETER); | |
| 864 | 3 | nStatesDim := Dimension.INTEGER(nStates, Variability.STRUCTURAL_PARAMETER); | |
| 865 | |||
| 866 | 3 | tTArrayBool := Type.ARRAY(Type.BOOLEAN(), {tDim}); | |
| 867 | 3 | tTArrayInt := Type.ARRAY(Type.INTEGER(), {tDim}); | |
| 868 | 3 | tArrayBool := Type.ARRAY(Type.BOOLEAN(), {nStatesDim}); | |
| 869 | 3 | tArrayInt := Type.ARRAY(Type.INTEGER(), {nStatesDim}); | |
| 870 | |||
| 871 | // ***** Parameter: nState ***** | ||
| 872 | 3 | nStatesRef := qCref("nState", Type.INTEGER(), {}, preRef); | |
| 873 | 3 | knowns := makeVarWithBinding(nStatesRef, Type.INTEGER(), Variability.STRUCTURAL_PARAMETER, | |
| 874 | Expression.INTEGER(nStates)) :: knowns; | ||
| 875 | |||
| 876 | // ***** Transition parameters (tFrom, tTo, tImmediate, tReset, tSynchronize, tPriority) ***** | ||
| 877 | i := 0; | ||
| 878 |
2/2✓ Branch 0 taken 5 times.
✓ Branch 1 taken 3 times.
|
8 | for tr in t loop |
| 879 | 5 | i := i + 1; | |
| 880 | 10 | tFromRefs := qCref("tFrom", tTArrayInt, {Subscript.INDEX(Expression.INTEGER(i))}, preRef) :: tFromRefs; | |
| 881 | 5 | knowns := makeVarWithBinding(listHead(tFromRefs), Type.INTEGER(), Variability.STRUCTURAL_PARAMETER, | |
| 882 | Expression.INTEGER(tr.from)) :: knowns; | ||
| 883 | |||
| 884 | 10 | tToRefs := qCref("tTo", tTArrayInt, {Subscript.INDEX(Expression.INTEGER(i))}, preRef) :: tToRefs; | |
| 885 | 5 | knowns := makeVarWithBinding(listHead(tToRefs), Type.INTEGER(), Variability.STRUCTURAL_PARAMETER, | |
| 886 | Expression.INTEGER(tr.to)) :: knowns; | ||
| 887 | |||
| 888 | 10 | tImmediateRefs := qCref("tImmediate", tTArrayBool, {Subscript.INDEX(Expression.INTEGER(i))}, preRef) :: tImmediateRefs; | |
| 889 | 5 | knowns := makeVarWithBinding(listHead(tImmediateRefs), Type.BOOLEAN(), Variability.STRUCTURAL_PARAMETER, | |
| 890 | Expression.BOOLEAN(tr.immediate)) :: knowns; | ||
| 891 | |||
| 892 | 10 | tResetRefs := qCref("tReset", tTArrayBool, {Subscript.INDEX(Expression.INTEGER(i))}, preRef) :: tResetRefs; | |
| 893 | 5 | knowns := makeVarWithBinding(listHead(tResetRefs), Type.BOOLEAN(), Variability.STRUCTURAL_PARAMETER, | |
| 894 | Expression.BOOLEAN(tr.reset)) :: knowns; | ||
| 895 | |||
| 896 | 10 | tSynchronizeRefs := qCref("tSynchronize", tTArrayBool, {Subscript.INDEX(Expression.INTEGER(i))}, preRef) :: tSynchronizeRefs; | |
| 897 | 5 | knowns := makeVarWithBinding(listHead(tSynchronizeRefs), Type.BOOLEAN(), Variability.STRUCTURAL_PARAMETER, | |
| 898 | Expression.BOOLEAN(tr.synchronize)) :: knowns; | ||
| 899 | |||
| 900 | 10 | tPriorityRefs := qCref("tPriority", tTArrayInt, {Subscript.INDEX(Expression.INTEGER(i))}, preRef) :: tPriorityRefs; | |
| 901 | 5 | knowns := makeVarWithBinding(listHead(tPriorityRefs), Type.INTEGER(), Variability.STRUCTURAL_PARAMETER, | |
| 902 | Expression.INTEGER(tr.priority)) :: knowns; | ||
| 903 | end for; | ||
| 904 | 3 | tFromRefs := listReverse(tFromRefs); | |
| 905 | 3 | tToRefs := listReverse(tToRefs); | |
| 906 | 3 | tImmediateRefs := listReverse(tImmediateRefs); | |
| 907 | 3 | tResetRefs := listReverse(tResetRefs); | |
| 908 | 3 | tSynchronizeRefs := listReverse(tSynchronizeRefs); | |
| 909 | 3 | tPriorityRefs := listReverse(tPriorityRefs); | |
| 910 | |||
| 911 | // ***** Condition variables c and cImmediate ***** | ||
| 912 | i := 0; | ||
| 913 |
2/2✓ Branch 0 taken 5 times.
✓ Branch 1 taken 3 times.
|
8 | for cExp in cExps loop |
| 914 | 5 | i := i + 1; | |
| 915 | 10 | cImmediateRefs := qCref("cImmediate", tTArrayBool, {Subscript.INDEX(Expression.INTEGER(i))}, preRef) :: cImmediateRefs; | |
| 916 | 10 | cRefs := qCref("c", tTArrayBool, {Subscript.INDEX(Expression.INTEGER(i))}, preRef) :: cRefs; | |
| 917 | 5 | vars := makeVarWithStart(listHead(cImmediateRefs), Type.BOOLEAN(), Variability.DISCRETE, Expression.BOOLEAN(false)) :: vars; | |
| 918 | 5 | vars := makeVar(listHead(cRefs), Type.BOOLEAN(), Variability.DISCRETE) :: vars; | |
| 919 | end for; | ||
| 920 | 3 | cImmediateRefs := listReverse(cImmediateRefs); | |
| 921 | 3 | cRefs := listReverse(cRefs); | |
| 922 | |||
| 923 | // ***** Scalar SMS variables ***** | ||
| 924 | 3 | activeRef := qCref("active", Type.BOOLEAN(), {}, preRef); | |
| 925 | 3 | vars := makeVar(activeRef, Type.BOOLEAN(), Variability.DISCRETE) :: vars; | |
| 926 | 3 | resetRef := qCref("reset", Type.BOOLEAN(), {}, preRef); | |
| 927 | 3 | vars := makeVar(resetRef, Type.BOOLEAN(), Variability.DISCRETE) :: vars; | |
| 928 | 3 | selectedStateRef := qCref("selectedState", Type.INTEGER(), {}, preRef); | |
| 929 | 3 | vars := makeVar(selectedStateRef, Type.INTEGER(), Variability.DISCRETE) :: vars; | |
| 930 | 3 | selectedResetRef := qCref("selectedReset", Type.BOOLEAN(), {}, preRef); | |
| 931 | 3 | vars := makeVar(selectedResetRef, Type.BOOLEAN(), Variability.DISCRETE) :: vars; | |
| 932 | 3 | firedRef := qCref("fired", Type.INTEGER(), {}, preRef); | |
| 933 | 3 | vars := makeVar(firedRef, Type.INTEGER(), Variability.DISCRETE) :: vars; | |
| 934 | 3 | activeStateRef := qCref("activeState", Type.INTEGER(), {}, preRef); | |
| 935 | 3 | vars := makeVar(activeStateRef, Type.INTEGER(), Variability.DISCRETE) :: vars; | |
| 936 | 3 | activeResetRef := qCref("activeReset", Type.BOOLEAN(), {}, preRef); | |
| 937 | 3 | vars := makeVar(activeResetRef, Type.BOOLEAN(), Variability.DISCRETE) :: vars; | |
| 938 | 3 | nextStateRef := qCref("nextState", Type.INTEGER(), {}, preRef); | |
| 939 | 3 | vars := makeVarWithStart(nextStateRef, Type.INTEGER(), Variability.DISCRETE, Expression.INTEGER(0)) :: vars; | |
| 940 | 3 | nextResetRef := qCref("nextReset", Type.BOOLEAN(), {}, preRef); | |
| 941 | 3 | vars := makeVarWithStart(nextResetRef, Type.BOOLEAN(), Variability.DISCRETE, Expression.BOOLEAN(false)) :: vars; | |
| 942 | |||
| 943 | // ***** Array variables sized by nStates ***** | ||
| 944 |
1/2✓ Branch 0 taken 3 times.
✗ Branch 1 not taken.
|
9 | for j in 1:nStates loop |
| 945 | 12 | activeResetStatesRefs := qCref("activeResetStates", tArrayBool, {Subscript.INDEX(Expression.INTEGER(j))}, preRef) :: activeResetStatesRefs; | |
| 946 | 6 | vars := makeVar(listHead(activeResetStatesRefs), Type.BOOLEAN(), Variability.DISCRETE) :: vars; | |
| 947 | 12 | nextResetStatesRefs := qCref("nextResetStates", tArrayBool, {Subscript.INDEX(Expression.INTEGER(j))}, preRef) :: nextResetStatesRefs; | |
| 948 | 6 | vars := makeVarWithStart(listHead(nextResetStatesRefs), Type.BOOLEAN(), Variability.DISCRETE, Expression.BOOLEAN(false)) :: vars; | |
| 949 | 12 | finalStatesRefs := qCref("finalStates", tArrayBool, {Subscript.INDEX(Expression.INTEGER(j))}, preRef) :: finalStatesRefs; | |
| 950 | 6 | vars := makeVar(listHead(finalStatesRefs), Type.BOOLEAN(), Variability.DISCRETE) :: vars; | |
| 951 | end for; | ||
| 952 | 3 | activeResetStatesRefs := listReverse(activeResetStatesRefs); | |
| 953 | 3 | nextResetStatesRefs := listReverse(nextResetStatesRefs); | |
| 954 | 3 | finalStatesRefs := listReverse(finalStatesRefs); | |
| 955 | 3 | stateMachineInFinalStateRef := qCref("stateMachineInFinalState", Type.BOOLEAN(), {}, preRef); | |
| 956 | 3 | vars := makeVar(stateMachineInFinalStateRef, Type.BOOLEAN(), Variability.DISCRETE) :: vars; | |
| 957 | |||
| 958 | // ***** Governing equations ***** | ||
| 959 | |||
| 960 | // cImmediate[i] = cExp[i]; c[i] = if immediate then cImmediate[i] else previous(cImmediate[i]) | ||
| 961 | i := 0; | ||
| 962 |
2/2✓ Branch 0 taken 5 times.
✓ Branch 1 taken 3 times.
|
8 | for cExp in cExps loop |
| 963 | 5 | i := i + 1; | |
| 964 | 5 | eqs := makeEq(makeCrefExp(listGet(cImmediateRefs, i), Type.BOOLEAN()), cExp, Type.BOOLEAN()) :: eqs; | |
| 965 | 5 | TRANSITION(immediate = immediateVal) := listGet(t, i); | |
| 966 |
1/2✗ Branch 0 not taken.
✓ Branch 1 taken 5 times.
|
5 | rhs := if immediateVal then |
| 967 | makeCrefExp(listGet(cImmediateRefs, i), Type.BOOLEAN()) | ||
| 968 | else | ||
| 969 | // Delayed: c[i] = if initial() then false else pre(cImmediate[i]) | ||
| 970 | // initial() guard prevents event-iteration cycling during initialization | ||
| 971 | makePreviousCall(makeCrefExp(listGet(cImmediateRefs, i), Type.BOOLEAN()), Type.BOOLEAN()); | ||
| 972 | 5 | eqs := makeEq(makeCrefExp(listGet(cRefs, i), Type.BOOLEAN()), rhs, Type.BOOLEAN()) :: eqs; | |
| 973 | end for; | ||
| 974 | |||
| 975 | // selectedState = if reset then 1 else previous(nextState) | ||
| 976 | 3 | eqs := makeEq( | |
| 977 | makeCrefExp(selectedStateRef, Type.INTEGER()), | ||
| 978 | makeIfExp( | ||
| 979 | makeCrefExp(resetRef, Type.BOOLEAN()), | ||
| 980 | Expression.INTEGER(1), | ||
| 981 | makePreviousCall(makeCrefExp(nextStateRef, Type.INTEGER()), Type.INTEGER()), | ||
| 982 | Type.INTEGER()), | ||
| 983 | Type.INTEGER()) :: eqs; | ||
| 984 | |||
| 985 | // selectedReset = if reset then true else previous(nextReset) | ||
| 986 | 3 | eqs := makeEq( | |
| 987 | makeCrefExp(selectedResetRef, Type.BOOLEAN()), | ||
| 988 | makeIfExp( | ||
| 989 | makeCrefExp(resetRef, Type.BOOLEAN()), | ||
| 990 | Expression.BOOLEAN(true), | ||
| 991 | makePreviousCall(makeCrefExp(nextResetRef, Type.BOOLEAN()), Type.BOOLEAN()), | ||
| 992 | Type.BOOLEAN()), | ||
| 993 | Type.BOOLEAN()) :: eqs; | ||
| 994 | |||
| 995 | // fired = max(if (t[i].from == selectedState) then c[i] else false) then i else 0 for i) | ||
| 996 | expLst := {}; | ||
| 997 |
1/2✓ Branch 0 taken 3 times.
✗ Branch 1 not taken.
|
8 | for j in 1:nTransitions loop |
| 998 | 5 | expCond := makeRelationEq( | |
| 999 | makeCrefExp(listGet(tFromRefs, j), Type.INTEGER()), | ||
| 1000 | makeCrefExp(selectedStateRef, Type.INTEGER()), | ||
| 1001 | Type.INTEGER()); | ||
| 1002 | 5 | expIf := makeIfExp(expCond, makeCrefExp(listGet(cRefs, j), Type.BOOLEAN()), Expression.BOOLEAN(false), Type.BOOLEAN()); | |
| 1003 | 5 | expLst := makeIfExp(expIf, Expression.INTEGER(j), Expression.INTEGER(0), Type.INTEGER()) :: expLst; | |
| 1004 | end for; | ||
| 1005 | 3 | expLst := listReverse(expLst); | |
| 1006 |
3/4✓ Branch 1 taken 2 times.
✓ Branch 2 taken 1 time.
✓ Branch 5 taken 1 time.
✗ Branch 6 not taken.
|
3 | rhs := if listLength(expLst) > 1 then |
| 1007 | makeMaxIntArrCall(expLst) | ||
| 1008 | elseif listLength(expLst) == 1 then listHead(expLst) | ||
| 1009 | else Expression.INTEGER(0); // no transitions: fired = 0 always | ||
| 1010 | 3 | eqs := makeEq(makeCrefExp(firedRef, Type.INTEGER()), rhs, Type.INTEGER()) :: eqs; | |
| 1011 | |||
| 1012 | // activeState = if reset then 1 elseif fired > 0 then t[fired].to else selectedState | ||
| 1013 | 3 | exp1 := makeRelationGt(makeCrefExp(firedRef, Type.INTEGER()), Expression.INTEGER(0), Type.INTEGER()); | |
| 1014 | 6 | exp2 := makeCrefExp(qCref("tTo", tTArrayInt, {Subscript.INDEX(makeCrefExp(firedRef, Type.INTEGER()))}, preRef), Type.INTEGER()); | |
| 1015 | 3 | expElse := makeIfExp(exp1, exp2, makeCrefExp(selectedStateRef, Type.INTEGER()), Type.INTEGER()); | |
| 1016 | 3 | eqs := makeEq( | |
| 1017 | makeCrefExp(activeStateRef, Type.INTEGER()), | ||
| 1018 | makeIfExp(makeCrefExp(resetRef, Type.BOOLEAN()), Expression.INTEGER(1), expElse, Type.INTEGER()), | ||
| 1019 | Type.INTEGER()) :: eqs; | ||
| 1020 | |||
| 1021 | // activeReset = if reset then true elseif fired > 0 then t[fired].reset else selectedReset | ||
| 1022 | 3 | exp1 := makeRelationGt(makeCrefExp(firedRef, Type.INTEGER()), Expression.INTEGER(0), Type.INTEGER()); | |
| 1023 | 6 | exp2 := makeCrefExp(qCref("tReset", tTArrayBool, {Subscript.INDEX(makeCrefExp(firedRef, Type.INTEGER()))}, preRef), Type.BOOLEAN()); | |
| 1024 | 3 | expElse := makeIfExp(exp1, exp2, makeCrefExp(selectedResetRef, Type.BOOLEAN()), Type.BOOLEAN()); | |
| 1025 | 3 | eqs := makeEq( | |
| 1026 | makeCrefExp(activeResetRef, Type.BOOLEAN()), | ||
| 1027 | makeIfExp(makeCrefExp(resetRef, Type.BOOLEAN()), Expression.BOOLEAN(true), expElse, Type.BOOLEAN()), | ||
| 1028 | Type.BOOLEAN()) :: eqs; | ||
| 1029 | |||
| 1030 | // nextState = if active then activeState else previous(nextState) | ||
| 1031 | 3 | eqs := makeEq( | |
| 1032 | makeCrefExp(nextStateRef, Type.INTEGER()), | ||
| 1033 | makeIfExp( | ||
| 1034 | makeCrefExp(activeRef, Type.BOOLEAN()), | ||
| 1035 | makeCrefExp(activeStateRef, Type.INTEGER()), | ||
| 1036 | makePreviousCall(makeCrefExp(nextStateRef, Type.INTEGER()), Type.INTEGER()), | ||
| 1037 | Type.INTEGER()), | ||
| 1038 | Type.INTEGER()) :: eqs; | ||
| 1039 | |||
| 1040 | // nextReset = if active then false else previous(nextReset) | ||
| 1041 | 3 | eqs := makeEq( | |
| 1042 | makeCrefExp(nextResetRef, Type.BOOLEAN()), | ||
| 1043 | makeIfExp( | ||
| 1044 | makeCrefExp(activeRef, Type.BOOLEAN()), | ||
| 1045 | Expression.BOOLEAN(false), | ||
| 1046 | makePreviousCall(makeCrefExp(nextResetRef, Type.BOOLEAN()), Type.BOOLEAN()), | ||
| 1047 | Type.BOOLEAN()), | ||
| 1048 | Type.BOOLEAN()) :: eqs; | ||
| 1049 | |||
| 1050 | // activeResetStates[i] = if reset then true else previous(nextResetStates[i]) | ||
| 1051 |
1/2✓ Branch 0 taken 3 times.
✗ Branch 1 not taken.
|
9 | for j in 1:nStates loop |
| 1052 | 6 | eqs := makeEq( | |
| 1053 | makeCrefExp(listGet(activeResetStatesRefs, j), Type.BOOLEAN()), | ||
| 1054 | makeIfExp( | ||
| 1055 | makeCrefExp(resetRef, Type.BOOLEAN()), | ||
| 1056 | Expression.BOOLEAN(true), | ||
| 1057 | makePreviousCall(makeCrefExp(listGet(nextResetStatesRefs, j), Type.BOOLEAN()), Type.BOOLEAN()), | ||
| 1058 | Type.BOOLEAN()), | ||
| 1059 | Type.BOOLEAN()) :: eqs; | ||
| 1060 | end for; | ||
| 1061 | |||
| 1062 | // nextResetStates[i] = if active then (if activeState == i then false else activeResetStates[i]) else previous(nextResetStates[i]) | ||
| 1063 |
1/2✓ Branch 0 taken 3 times.
✗ Branch 1 not taken.
|
9 | for j in 1:nStates loop |
| 1064 | 6 | exp1 := makeRelationEq(makeCrefExp(activeStateRef, Type.INTEGER()), Expression.INTEGER(j), Type.INTEGER()); | |
| 1065 | 6 | expThen := makeIfExp(exp1, Expression.BOOLEAN(false), makeCrefExp(listGet(activeResetStatesRefs, j), Type.BOOLEAN()), Type.BOOLEAN()); | |
| 1066 | 6 | expElse := makePreviousCall(makeCrefExp(listGet(nextResetStatesRefs, j), Type.BOOLEAN()), Type.BOOLEAN()); | |
| 1067 | 6 | eqs := makeEq( | |
| 1068 | makeCrefExp(listGet(nextResetStatesRefs, j), Type.BOOLEAN()), | ||
| 1069 | makeIfExp(makeCrefExp(activeRef, Type.BOOLEAN()), expThen, expElse, Type.BOOLEAN()), | ||
| 1070 | Type.BOOLEAN()) :: eqs; | ||
| 1071 | end for; | ||
| 1072 | |||
| 1073 | // finalStates[i] = max(if t[j].from == i then 1 else 0 for j) == 0 | ||
| 1074 |
1/2✓ Branch 0 taken 3 times.
✗ Branch 1 not taken.
|
9 | for j in 1:nStates loop |
| 1075 | expLst := {}; | ||
| 1076 |
1/2✓ Branch 0 taken 6 times.
✗ Branch 1 not taken.
|
16 | for k in 1:nTransitions loop |
| 1077 | 10 | expCond := makeRelationEq(makeCrefExp(listGet(tFromRefs, k), Type.INTEGER()), Expression.INTEGER(j), Type.INTEGER()); | |
| 1078 | 10 | expLst := makeIfExp(expCond, Expression.INTEGER(1), Expression.INTEGER(0), Type.INTEGER()) :: expLst; | |
| 1079 | end for; | ||
| 1080 | 6 | expLst := listReverse(expLst); | |
| 1081 | // With no outgoing transitions, finalStates[i] = true (state is a final state) | ||
| 1082 |
3/4✓ Branch 1 taken 4 times.
✓ Branch 2 taken 2 times.
✓ Branch 6 taken 2 times.
✗ Branch 7 not taken.
|
6 | rhs := if listLength(expLst) > 1 then |
| 1083 | makeRelationEq(makeMaxIntArrCall(expLst), Expression.INTEGER(0), Type.INTEGER()) | ||
| 1084 | elseif listLength(expLst) == 1 then | ||
| 1085 | makeRelationEq(listHead(expLst), Expression.INTEGER(0), Type.INTEGER()) | ||
| 1086 | else | ||
| 1087 | Expression.BOOLEAN(true); | ||
| 1088 | 6 | eqs := makeEq(makeCrefExp(listGet(finalStatesRefs, j), Type.BOOLEAN()), rhs, Type.BOOLEAN()) :: eqs; | |
| 1089 | end for; | ||
| 1090 | |||
| 1091 | // stateMachineInFinalState = finalStates[activeState] | ||
| 1092 | 6 | eqs := makeEq( | |
| 1093 | makeCrefExp(stateMachineInFinalStateRef, Type.BOOLEAN()), | ||
| 1094 | makeCrefExp(qCref("finalStates", tArrayBool, {Subscript.INDEX(makeCrefExp(activeStateRef, Type.INTEGER()))}, preRef), Type.BOOLEAN()), | ||
| 1095 | Type.BOOLEAN()) :: eqs; | ||
| 1096 | |||
| 1097 | 3 | sem := FLAT_SM_SEMANTICS( | |
| 1098 | initStateCref, | ||
| 1099 | listArray(stateCrefs), | ||
| 1100 | t, cExps, | ||
| 1101 | vars, knowns, eqs, {}, {}, NONE()); | ||
| 1102 | end basicFlatSmSemantics; | ||
| 1103 | |||
| 1104 | // ============================================================ | ||
| 1105 | // addPropagationEquations | ||
| 1106 | // ============================================================ | ||
| 1107 | |||
| 1108 | protected | ||
| 1109 | function addPropagationEquations | ||
| 1110 | "Add activation/reset propagation variables and equations." | ||
| 1111 | input FlatSmSemantics inSem; | ||
| 1112 | input Option<ComponentRef> enclosingStateCrefOpt; | ||
| 1113 | input Option<FlatSmSemantics> enclosingSmSemOpt; | ||
| 1114 | output FlatSmSemantics outSem = inSem; | ||
| 1115 | protected | ||
| 1116 | ComponentRef preRef, initStateRef, activeRef, resetRef, initRef; | ||
| 1117 | list<Variable> pvars = {}; | ||
| 1118 | list<Equation> peqs = {}; | ||
| 1119 | Integer nStates, posOfEnclosing; | ||
| 1120 | Type tArrayBool; | ||
| 1121 | |||
| 1122 | // Enclosing SM fields | ||
| 1123 | ComponentRef enclosingStateCref, enclosingPreRef, enclosingActiveResetStateRef, | ||
| 1124 | enclosingActiveResetRef, enclosingActiveStateRef, enclosingInitStateRef; | ||
| 1125 | FlatSmSemantics enclosingSem; | ||
| 1126 | array<ComponentRef> enclosingComps; | ||
| 1127 | |||
| 1128 | // Per-state indicator variables | ||
| 1129 | ComponentRef stateRef, activePlotRef; | ||
| 1130 | Variable activePlotVar, ticksVar, timeEnteredVar, timeInVar; | ||
| 1131 | Equation activePlotEq, ticksEq, timeEnteredEq, timeInEq; | ||
| 1132 | algorithm | ||
| 1133 | 3 | initStateRef := inSem.initStateRef; | |
| 1134 | 3 | preRef := makeSMSPrefix(initStateRef); | |
| 1135 | 3 | activeRef := qCref("active", Type.BOOLEAN(), {}, preRef); | |
| 1136 | 3 | resetRef := qCref("reset", Type.BOOLEAN(), {}, preRef); | |
| 1137 |
1/2✗ Branch 0 not taken.
✓ Branch 1 taken 3 times.
|
3 | nStates := arrayLength(inSem.smComps); |
| 1138 | 6 | tArrayBool := Type.ARRAY(Type.BOOLEAN(), {Dimension.INTEGER(nStates, Variability.STRUCTURAL_PARAMETER)}); | |
| 1139 | |||
| 1140 |
2/4✗ Branch 0 not taken.
✓ Branch 1 taken 3 times.
✓ Branch 2 taken 3 times.
✗ Branch 3 not taken.
|
3 | if isNone(enclosingSmSemOpt) then |
| 1141 | // Toplevel SM: self-reset at first clock tick | ||
| 1142 | 3 | initRef := qCref("init", Type.BOOLEAN(), {}, preRef); | |
| 1143 | 3 | pvars := makeVarWithStart(initRef, Type.BOOLEAN(), Variability.DISCRETE, Expression.BOOLEAN(true)) :: pvars; | |
| 1144 | 3 | peqs := makeEq(makeCrefExp(initRef, Type.BOOLEAN()), Expression.BOOLEAN(false), Type.BOOLEAN()) :: peqs; | |
| 1145 | // reset = initial() or pre(init) -- initial() guard prevents event-iteration cycling | ||
| 1146 | 3 | peqs := makeEq( | |
| 1147 | makeCrefExp(resetRef, Type.BOOLEAN()), | ||
| 1148 | makePreviousCall(makeCrefExp(initRef, Type.BOOLEAN()), Type.BOOLEAN()), Type.BOOLEAN()) :: peqs; | ||
| 1149 | // active = true (toplevel SM always active) | ||
| 1150 | 3 | peqs := makeEq(makeCrefExp(activeRef, Type.BOOLEAN()), Expression.BOOLEAN(true), Type.BOOLEAN()) :: peqs; | |
| 1151 | else | ||
| 1152 | // Nested SM: propagate from enclosing SM | ||
| 1153 | ✗ | SOME(enclosingStateCref) := enclosingStateCrefOpt; | |
| 1154 | ✗ | SOME(enclosingSem) := enclosingSmSemOpt; | |
| 1155 | ✗ | enclosingComps := enclosingSem.smComps; | |
| 1156 | enclosingInitStateRef := arrayGet(enclosingComps, 1); | ||
| 1157 | ✗ | enclosingPreRef := makeSMSPrefix(enclosingInitStateRef); | |
| 1158 | |||
| 1159 | posOfEnclosing := 1; | ||
| 1160 | ✗ | for sc in arrayList(enclosingComps) loop | |
| 1161 | ✗ | if ComponentRef.isEqual(sc, enclosingStateCref) then break; end if; | |
| 1162 | ✗ | posOfEnclosing := posOfEnclosing + 1; | |
| 1163 | end for; | ||
| 1164 | |||
| 1165 | ✗ | enclosingActiveStateRef := qCref("activeState", Type.INTEGER(), {}, enclosingPreRef); | |
| 1166 | ✗ | enclosingActiveResetRef := qCref("activeReset", Type.BOOLEAN(), {}, enclosingPreRef); | |
| 1167 | ✗ | enclosingActiveResetStateRef := qCref("activeResetStates", tArrayBool, | |
| 1168 | {Subscript.INDEX(Expression.INTEGER(posOfEnclosing))}, enclosingPreRef); | ||
| 1169 | |||
| 1170 | // reset = activeResetStates[pos] or (activeReset and activeState == pos) | ||
| 1171 | ✗ | peqs := makeEq( | |
| 1172 | makeCrefExp(resetRef, Type.BOOLEAN()), | ||
| 1173 | Expression.LBINARY( | ||
| 1174 | makeCrefExp(enclosingActiveResetStateRef, Type.BOOLEAN()), | ||
| 1175 | Operator.makeOr(Type.BOOLEAN()), | ||
| 1176 | Expression.LBINARY( | ||
| 1177 | makeCrefExp(enclosingActiveResetRef, Type.BOOLEAN()), | ||
| 1178 | Operator.makeAnd(Type.BOOLEAN()), | ||
| 1179 | makeRelationEq(makeCrefExp(enclosingActiveStateRef, Type.INTEGER()), | ||
| 1180 | Expression.INTEGER(posOfEnclosing), Type.INTEGER()))), | ||
| 1181 | Type.BOOLEAN()) :: peqs; | ||
| 1182 | |||
| 1183 | // active = (activeState == pos) | ||
| 1184 | ✗ | peqs := makeEq( | |
| 1185 | makeCrefExp(activeRef, Type.BOOLEAN()), | ||
| 1186 | makeRelationEq(makeCrefExp(enclosingActiveStateRef, Type.INTEGER()), | ||
| 1187 | Expression.INTEGER(posOfEnclosing), Type.INTEGER()), | ||
| 1188 | Type.BOOLEAN()) :: peqs; | ||
| 1189 | end if; | ||
| 1190 | |||
| 1191 | // Per-state: active indicator, ticksInState, timeEnteredState, timeInState | ||
| 1192 |
1/2✓ Branch 0 taken 3 times.
✗ Branch 1 not taken.
|
9 | for j in 1:nStates loop |
| 1193 | 6 | stateRef := arrayGet(inSem.smComps, j); | |
| 1194 | 6 | (activePlotVar, activePlotEq) := createActiveIndicator(stateRef, preRef, j); | |
| 1195 | pvars := activePlotVar :: pvars; | ||
| 1196 | 6 | peqs := activePlotEq :: peqs; | |
| 1197 | |||
| 1198 | 6 | activePlotRef := activePlotVar.name; | |
| 1199 | 6 | (ticksVar, ticksEq) := createTicksInStateIndicator(stateRef, activePlotRef); | |
| 1200 | pvars := ticksVar :: pvars; | ||
| 1201 | 6 | peqs := ticksEq :: peqs; | |
| 1202 | |||
| 1203 | 6 | (timeEnteredVar, timeEnteredEq) := createTimeEnteredStateIndicator(stateRef, activePlotRef); | |
| 1204 | 6 | (timeInVar, timeInEq) := createTimeInStateIndicator(stateRef, activePlotRef, timeEnteredVar); | |
| 1205 | pvars := timeEnteredVar :: timeInVar :: pvars; | ||
| 1206 | 6 | peqs := timeEnteredEq :: timeInEq :: peqs; | |
| 1207 | end for; | ||
| 1208 | |||
| 1209 | 3 | outSem.pvars := pvars; | |
| 1210 | outSem.peqs := peqs; | ||
| 1211 | outSem.enclosingState := enclosingStateCrefOpt; | ||
| 1212 | end addPropagationEquations; | ||
| 1213 | |||
| 1214 | // ============================================================ | ||
| 1215 | // elabXInStateOps | ||
| 1216 | // ============================================================ | ||
| 1217 | |||
| 1218 | protected | ||
| 1219 | function elabXInStateOps | ||
| 1220 | "Elaborate ticksInState() and timeInState() in transition conditions." | ||
| 1221 | input output FlatSmSemantics sem; | ||
| 1222 | input Option<ComponentRef> enclosingStateCrefOpt; | ||
| 1223 | protected | ||
| 1224 | list<Transition> tElab = {}; | ||
| 1225 | list<Expression> cElab = {}; | ||
| 1226 | Integer i; | ||
| 1227 | ComponentRef stateRef; | ||
| 1228 | Expression substTickExp, substTimeExp, c3, c4; | ||
| 1229 | Boolean found; | ||
| 1230 | Transition curT; | ||
| 1231 | Integer curFrom, curTo, curPriority; | ||
| 1232 | Boolean curImmediate, curReset, curSynchronize; | ||
| 1233 | algorithm | ||
| 1234 | i := 0; | ||
| 1235 |
2/2✓ Branch 1 taken 5 times.
✓ Branch 2 taken 3 times.
|
8 | for tc in List.zip(sem.t, sem.c) loop |
| 1236 | 5 | i := i + 1; | |
| 1237 | 5 | (_, c3) := tc; | |
| 1238 | 5 | curT := listGet(sem.t, i); | |
| 1239 | 5 | TRANSITION(from = curFrom, to = curTo, immediate = curImmediate, | |
| 1240 | reset = curReset, synchronize = curSynchronize, priority = curPriority) := curT; | ||
| 1241 | 5 | stateRef := arrayGet(sem.smComps, curFrom); | |
| 1242 | |||
| 1243 | 5 | substTickExp := makeCrefExp(qCref("$ticksInState", Type.INTEGER(), {}, stateRef), Type.INTEGER()); | |
| 1244 | 5 | (c4, found) := subsXInState(c3, "ticksInState", substTickExp); | |
| 1245 |
1/6✗ Branch 0 not taken.
✓ Branch 1 taken 5 times.
✗ Branch 2 not taken.
✗ Branch 3 not taken.
✗ Branch 4 not taken.
✗ Branch 5 not taken.
|
5 | if found and isSome(enclosingStateCrefOpt) then |
| 1246 | ✗ | Error.addCompilerError("Found 'ticksInState()' within a state of a hierarchical state machine."); | |
| 1247 | ✗ | fail(); | |
| 1248 | end if; | ||
| 1249 |
1/2✗ Branch 0 not taken.
✓ Branch 1 taken 5 times.
|
5 | if found then |
| 1250 | ✗ | sem.eqs := list(smeqsSubsXInState(eq, arrayGet(sem.smComps, 1), i, listLength(sem.t), substTickExp, "ticksInState") for eq in sem.eqs); | |
| 1251 | end if; | ||
| 1252 | |||
| 1253 | 5 | substTimeExp := makeCrefExp(qCref("$timeInState", Type.REAL(), {}, stateRef), Type.REAL()); | |
| 1254 | 5 | (c4, found) := subsXInState(c4, "timeInState", substTimeExp); | |
| 1255 |
4/6✓ Branch 0 taken 2 times.
✓ Branch 1 taken 3 times.
✗ Branch 2 not taken.
✓ Branch 3 taken 2 times.
✗ Branch 4 not taken.
✓ Branch 5 taken 2 times.
|
5 | if found and isSome(enclosingStateCrefOpt) then |
| 1256 | ✗ | Error.addCompilerError("Found 'timeInState()' within a state of a hierarchical state machine."); | |
| 1257 | ✗ | fail(); | |
| 1258 | end if; | ||
| 1259 |
2/2✓ Branch 0 taken 2 times.
✓ Branch 1 taken 3 times.
|
5 | if found then |
| 1260 |
5/6✓ Branch 0 taken 36 times.
✓ Branch 1 taken 2 times.
✓ Branch 2 taken 36 times.
✓ Branch 3 taken 2 times.
✗ Branch 5 not taken.
✓ Branch 6 taken 36 times.
|
76 | sem.eqs := list(smeqsSubsXInState(eq, arrayGet(sem.smComps, 1), i, listLength(sem.t), substTimeExp, "timeInState") for eq in sem.eqs); |
| 1261 | end if; | ||
| 1262 | |||
| 1263 |
3/6✓ Branch 0 taken 5 times.
✗ Branch 1 not taken.
✗ Branch 2 not taken.
✓ Branch 3 taken 5 times.
✓ Branch 4 taken 5 times.
✗ Branch 5 not taken.
|
15 | tElab := TRANSITION(curFrom, curTo, c4, curImmediate, curReset, curSynchronize, curPriority) :: tElab; |
| 1264 | cElab := c4 :: cElab; | ||
| 1265 | end for; | ||
| 1266 | 3 | sem.t := listReverse(tElab); | |
| 1267 | sem.c := listReverse(cElab); | ||
| 1268 | end elabXInStateOps; | ||
| 1269 | |||
| 1270 | protected | ||
| 1271 | function subsXInState | ||
| 1272 | "Find and replace xInState() in expression." | ||
| 1273 | input Expression inExp; | ||
| 1274 | input String funcName; | ||
| 1275 | input Expression substExp; | ||
| 1276 | output Expression outExp; | ||
| 1277 | output Boolean found = false; | ||
| 1278 | algorithm | ||
| 1279 |
2/2✓ Branch 3 taken 10 times.
✓ Branch 4 taken 2 times.
|
12 | (outExp, found) := Expression.mapFold(inExp, |
| 1280 | function subsXInStateHelper(funcName = funcName, substExp = substExp), false); | ||
| 1281 | end subsXInState; | ||
| 1282 | |||
| 1283 | protected | ||
| 1284 | function subsXInStateHelper | ||
| 1285 | input output Expression exp; | ||
| 1286 | input String funcName; | ||
| 1287 | input Expression substExp; | ||
| 1288 | input output Boolean found; | ||
| 1289 | protected | ||
| 1290 | Call expCall; | ||
| 1291 | algorithm | ||
| 1292 | try | ||
| 1293 |
2/2✓ Branch 0 taken 26 times.
✓ Branch 1 taken 6 times.
|
32 | Expression.CALL(call = expCall) := exp; |
| 1294 |
3/4✓ Branch 1 taken 4 times.
✓ Branch 2 taken 2 times.
✗ Branch 5 not taken.
✓ Branch 6 taken 4 times.
|
6 | if not stringEq(Call.functionNameLast(expCall), funcName) then fail(); end if; |
| 1295 |
1/2✗ Branch 1 not taken.
✓ Branch 2 taken 4 times.
|
4 | if not listEmpty(Call.arguments(expCall)) then fail(); end if; |
| 1296 | exp := substExp; | ||
| 1297 | found := true; | ||
| 1298 | else | ||
| 1299 | end try; | ||
| 1300 | end subsXInStateHelper; | ||
| 1301 | |||
| 1302 | protected | ||
| 1303 | function smeqsSubsXInState | ||
| 1304 | "Replace xInState() in a specific transition's semantic equation." | ||
| 1305 | input Equation eq; | ||
| 1306 | input ComponentRef initStateComp; | ||
| 1307 | input Integer i; | ||
| 1308 | input Integer nTransitions; | ||
| 1309 | input Expression substExp; | ||
| 1310 | input String xInState; | ||
| 1311 | output Equation outEq = eq; | ||
| 1312 | protected | ||
| 1313 | ComponentRef preRef, lhsRef, cRef; | ||
| 1314 | Type tArrayBool; | ||
| 1315 | Expression lhs, rhs, newRhs; | ||
| 1316 | algorithm | ||
| 1317 | outEq := match eq | ||
| 1318 | case Equation.EQUALITY() | ||
| 1319 | algorithm | ||
| 1320 | 36 | preRef := makeSMSPrefix(initStateComp); | |
| 1321 | 72 | tArrayBool := Type.ARRAY(Type.BOOLEAN(), {Dimension.INTEGER(nTransitions, Variability.STRUCTURAL_PARAMETER)}); | |
| 1322 | 72 | cRef := qCref("cImmediate", tArrayBool, {Subscript.INDEX(Expression.INTEGER(i))}, preRef); | |
| 1323 |
1/2✗ Branch 0 not taken.
✓ Branch 1 taken 36 times.
|
36 | Expression.CREF(cref = lhsRef) := eq.lhs; |
| 1324 |
2/2✓ Branch 1 taken 2 times.
✓ Branch 2 taken 34 times.
|
36 | if ComponentRef.isEqual(cRef, lhsRef) then |
| 1325 | 2 | (newRhs, _) := subsXInState(eq.rhs, xInState, substExp); | |
| 1326 | 2 | outEq := Equation.EQUALITY(eq.lhs, newRhs, eq.ty, eq.scope, eq.source, ScalarizeMode.NO_PREFERENCE); | |
| 1327 | end if; | ||
| 1328 | then outEq; | ||
| 1329 | else eq; | ||
| 1330 | end match; | ||
| 1331 | end smeqsSubsXInState; | ||
| 1332 | |||
| 1333 | // ============================================================ | ||
| 1334 | // State indicator helpers | ||
| 1335 | // ============================================================ | ||
| 1336 | |||
| 1337 | protected | ||
| 1338 | function createActiveIndicator | ||
| 1339 | "Create stateRef.active variable and equation: active = smOf.init.active and (activeState == i)" | ||
| 1340 | input ComponentRef stateRef; | ||
| 1341 | input ComponentRef preRef; | ||
| 1342 | input Integer i; | ||
| 1343 | output Variable activePlotVar; | ||
| 1344 | output Equation eqn; | ||
| 1345 | protected | ||
| 1346 | ComponentRef activePlotRef, activeRef, activeStateRef; | ||
| 1347 | Expression andExp, eqExp; | ||
| 1348 | algorithm | ||
| 1349 | 6 | activePlotRef := qCref("active", Type.BOOLEAN(), {}, stateRef); | |
| 1350 | 6 | activePlotVar := makeVarWithStart(activePlotRef, Type.BOOLEAN(), Variability.DISCRETE, Expression.BOOLEAN(false)); | |
| 1351 | 6 | activeRef := qCref("active", Type.BOOLEAN(), {}, preRef); | |
| 1352 | 6 | activeStateRef := qCref("activeState", Type.INTEGER(), {}, preRef); | |
| 1353 | 6 | eqExp := makeRelationEq(makeCrefExp(activeStateRef, Type.INTEGER()), Expression.INTEGER(i), Type.INTEGER()); | |
| 1354 | 6 | andExp := Expression.LBINARY(makeCrefExp(activeRef, Type.BOOLEAN()), Operator.makeAnd(Type.BOOLEAN()), eqExp); | |
| 1355 | 6 | eqn := makeEq(makeCrefExp(activePlotRef, Type.BOOLEAN()), andExp, Type.BOOLEAN()); | |
| 1356 | end createActiveIndicator; | ||
| 1357 | |||
| 1358 | protected | ||
| 1359 | function createTicksInStateIndicator | ||
| 1360 | "Create stateRef.$ticksInState = if active then previous($ticksInState)+1 else 0" | ||
| 1361 | input ComponentRef stateRef; | ||
| 1362 | input ComponentRef stateActiveRef; | ||
| 1363 | output Variable ticksVar; | ||
| 1364 | output Equation ticksEq; | ||
| 1365 | protected | ||
| 1366 | ComponentRef ticksRef; | ||
| 1367 | Expression ticksExp, expCond, expThen, expElse; | ||
| 1368 | algorithm | ||
| 1369 | 6 | ticksRef := qCref("$ticksInState", Type.INTEGER(), {}, stateRef); | |
| 1370 | 6 | ticksVar := makeVarWithStart(ticksRef, Type.INTEGER(), Variability.DISCRETE, Expression.INTEGER(0)); | |
| 1371 | 6 | ticksExp := makeCrefExp(ticksRef, Type.INTEGER()); | |
| 1372 | // $ticksInState = if initial() or not active then 0 else pre($ticksInState) + 1 | ||
| 1373 | 6 | expCond := Expression.LUNARY(Operator.makeNot(Type.BOOLEAN()), makeCrefExp(stateActiveRef, Type.BOOLEAN())); | |
| 1374 | expThen := Expression.INTEGER(0); | ||
| 1375 | 6 | expElse := Expression.BINARY( | |
| 1376 | makePreviousCall(ticksExp, Type.INTEGER()), | ||
| 1377 | Operator.makeAdd(Type.INTEGER()), | ||
| 1378 | Expression.INTEGER(1)); | ||
| 1379 | 6 | ticksEq := makeEq(ticksExp, makeIfExp(expCond, expThen, expElse, Type.INTEGER()), Type.INTEGER()); | |
| 1380 | end createTicksInStateIndicator; | ||
| 1381 | |||
| 1382 | protected | ||
| 1383 | function createTimeEnteredStateIndicator | ||
| 1384 | "Create $timeEnteredState = if (not previous(active) and active) then sample(time) else previous($timeEnteredState)" | ||
| 1385 | input ComponentRef stateRef; | ||
| 1386 | input ComponentRef stateActiveRef; | ||
| 1387 | output Variable timeEnteredVar; | ||
| 1388 | output Equation timeEnteredEq; | ||
| 1389 | protected | ||
| 1390 | ComponentRef timeEnteredRef; | ||
| 1391 | Expression timeEnteredExp, expCond, expThen, expElse, activeExp; | ||
| 1392 | algorithm | ||
| 1393 | 6 | timeEnteredRef := qCref("$timeEnteredState", Type.REAL(), {}, stateRef); | |
| 1394 | 6 | timeEnteredVar := makeVarWithStart(timeEnteredRef, Type.REAL(), Variability.CONTINUOUS, Expression.REAL(0.0)); | |
| 1395 | 6 | timeEnteredExp := makeCrefExp(timeEnteredRef, Type.REAL()); | |
| 1396 | 6 | activeExp := makeCrefExp(stateActiveRef, Type.BOOLEAN()); | |
| 1397 | // previous(active) == false and active == true | ||
| 1398 | 6 | expCond := Expression.LBINARY( | |
| 1399 | makeRelationEq(makePreviousCall(activeExp, Type.BOOLEAN()), Expression.BOOLEAN(false), Type.BOOLEAN()), | ||
| 1400 | Operator.makeAnd(Type.BOOLEAN()), | ||
| 1401 | makeRelationEq(activeExp, Expression.BOOLEAN(true), Type.BOOLEAN())); | ||
| 1402 | // sample(time, Clock()) - using inferred clock | ||
| 1403 | 6 | expThen := makeSampleTimeCall(); | |
| 1404 | 6 | expElse := makePreviousCall(timeEnteredExp, Type.REAL()); | |
| 1405 | 6 | timeEnteredEq := makeEq(timeEnteredExp, makeIfExp(expCond, expThen, expElse, Type.REAL()), Type.REAL()); | |
| 1406 | end createTimeEnteredStateIndicator; | ||
| 1407 | |||
| 1408 | protected | ||
| 1409 | function createTimeInStateIndicator | ||
| 1410 | "Create $timeInState = if active then sample(time) - $timeEnteredState else 0" | ||
| 1411 | input ComponentRef stateRef; | ||
| 1412 | input ComponentRef stateActiveRef; | ||
| 1413 | input Variable timeEnteredVar; | ||
| 1414 | output Variable timeInVar; | ||
| 1415 | output Equation timeInEq; | ||
| 1416 | protected | ||
| 1417 | ComponentRef timeInRef; | ||
| 1418 | Expression timeInExp, expCond, expThen, expElse, timeEnteredExp; | ||
| 1419 | algorithm | ||
| 1420 | 6 | timeInRef := qCref("$timeInState", Type.REAL(), {}, stateRef); | |
| 1421 | 6 | timeInVar := makeVarWithStart(timeInRef, Type.REAL(), Variability.CONTINUOUS, Expression.REAL(0.0)); | |
| 1422 | 6 | timeInExp := makeCrefExp(timeInRef, Type.REAL()); | |
| 1423 | 6 | timeEnteredExp := makeCrefExp(timeEnteredVar.name, Type.REAL()); | |
| 1424 | 6 | expCond := makeCrefExp(stateActiveRef, Type.BOOLEAN()); | |
| 1425 | 6 | expThen := Expression.BINARY(makeSampleTimeCall(), Operator.makeSub(Type.REAL()), timeEnteredExp); | |
| 1426 | expElse := Expression.REAL(0.0); | ||
| 1427 | 6 | timeInEq := makeEq(timeInExp, makeIfExp(expCond, expThen, expElse, Type.REAL()), Type.REAL()); | |
| 1428 | end createTimeInStateIndicator; | ||
| 1429 | |||
| 1430 | // ============================================================ | ||
| 1431 | // Reset and activation wrapping | ||
| 1432 | // ============================================================ | ||
| 1433 | |||
| 1434 | protected | ||
| 1435 | function wrapInStateActivationConditional | ||
| 1436 | "Transform a.x = e → a.x = if a.active then e else (x_previous or previous(a.x))" | ||
| 1437 | input Equation inEq; | ||
| 1438 | input ComponentRef stateCref; | ||
| 1439 | input Boolean isResetEquation; | ||
| 1440 | output Equation outEq; | ||
| 1441 | protected | ||
| 1442 | Expression lhs, rhs, activeRef, expElse; | ||
| 1443 | ComponentRef lhsCref; | ||
| 1444 | Type ty; | ||
| 1445 | NFInstNode.ScopeRef eqScope; | ||
| 1446 | DAE.ElementSource eqSource; | ||
| 1447 | algorithm | ||
| 1448 |
1/2✗ Branch 0 not taken.
✓ Branch 1 taken 4 times.
|
4 | Equation.EQUALITY(lhs = lhs, rhs = rhs, ty = ty, scope = eqScope, source = eqSource) := inEq; |
| 1449 |
1/2✗ Branch 0 not taken.
✓ Branch 1 taken 4 times.
|
4 | Expression.CREF(ty = ty, cref = lhsCref) := lhs; |
| 1450 | 4 | activeRef := makeCrefExp(qCref("active", Type.BOOLEAN(), {}, stateCref), Type.BOOLEAN()); | |
| 1451 |
1/2✗ Branch 0 not taken.
✓ Branch 1 taken 4 times.
|
4 | if isResetEquation then |
| 1452 | ✗ | expElse := makeCrefExp( | |
| 1453 | ComponentRef.prefixCref( | ||
| 1454 | InstNode.NAME_NODE(ComponentRef.firstName(lhsCref) + "_previous"), | ||
| 1455 | ty, {}, ComponentRef.rest(lhsCref)), | ||
| 1456 | ty); | ||
| 1457 | else | ||
| 1458 | 4 | expElse := makePreviousCall(lhs, ty); | |
| 1459 | end if; | ||
| 1460 | 4 | outEq := Equation.EQUALITY(lhs, makeIfExp(activeRef, rhs, expElse, ty), ty, eqScope, eqSource, ScalarizeMode.NO_PREFERENCE); | |
| 1461 | end wrapInStateActivationConditional; | ||
| 1462 | |||
| 1463 | protected | ||
| 1464 | function createResetEquation | ||
| 1465 | "Create: x_previous = if active and (activeReset or activeResetStates[i]) then x_start else previous(x)" | ||
| 1466 | input ComponentRef lhsCref; | ||
| 1467 | input Type lhsTy; | ||
| 1468 | input ComponentRef stateCref; | ||
| 1469 | input FlatSmSemantics sem; | ||
| 1470 | input UnorderedMap<ComponentRef, Expression> crToStart; | ||
| 1471 | output Equation outEq; | ||
| 1472 | protected | ||
| 1473 | ComponentRef preRef, initStateRef; | ||
| 1474 | Expression activeExp, activeResetExp, activeResetStatesExp, orExp, andExp, prevExp, startExp, ifExp, lhsPrevExp; | ||
| 1475 | Integer i, nStates; | ||
| 1476 | Type tArrayBool; | ||
| 1477 | algorithm | ||
| 1478 | ✗ | initStateRef := arrayGet(sem.smComps, 1); | |
| 1479 | ✗ | preRef := makeSMSPrefix(initStateRef); | |
| 1480 | i := 1; | ||
| 1481 | ✗ | for sc in arrayList(sem.smComps) loop | |
| 1482 | ✗ | if ComponentRef.isEqual(sc, stateCref) then break; end if; | |
| 1483 | ✗ | i := i + 1; | |
| 1484 | end for; | ||
| 1485 | ✗ | nStates := arrayLength(sem.smComps); | |
| 1486 | ✗ | tArrayBool := Type.ARRAY(Type.BOOLEAN(), {Dimension.INTEGER(nStates, Variability.STRUCTURAL_PARAMETER)}); | |
| 1487 | |||
| 1488 | ✗ | activeResetExp := makeCrefExp(qCref("activeReset", Type.BOOLEAN(), {}, preRef), Type.BOOLEAN()); | |
| 1489 | ✗ | activeResetStatesExp := makeCrefExp(qCref("activeResetStates", tArrayBool, | |
| 1490 | {Subscript.INDEX(Expression.INTEGER(i))}, preRef), Type.BOOLEAN()); | ||
| 1491 | ✗ | orExp := Expression.LBINARY(activeResetExp, Operator.makeOr(Type.BOOLEAN()), activeResetStatesExp); | |
| 1492 | ✗ | activeExp := makeCrefExp(qCref("active", Type.BOOLEAN(), {}, stateCref), Type.BOOLEAN()); | |
| 1493 | ✗ | andExp := Expression.LBINARY(activeExp, Operator.makeAnd(Type.BOOLEAN()), orExp); | |
| 1494 | ✗ | prevExp := makePreviousCall(makeCrefExp(lhsCref, lhsTy), lhsTy); | |
| 1495 | |||
| 1496 | ✗ | startExp := UnorderedMap.getOrDefault(lhsCref, crToStart, Expression.INTEGER(0)); | |
| 1497 | |||
| 1498 | ✗ | ifExp := makeIfExp(andExp, startExp, prevExp, lhsTy); | |
| 1499 | ✗ | lhsPrevExp := makeCrefExp( | |
| 1500 | ComponentRef.prefixCref( | ||
| 1501 | InstNode.NAME_NODE(ComponentRef.firstName(lhsCref) + "_previous"), | ||
| 1502 | lhsTy, {}, ComponentRef.rest(lhsCref)), | ||
| 1503 | lhsTy); | ||
| 1504 | ✗ | outEq := makeEq(lhsPrevExp, ifExp, lhsTy); | |
| 1505 | end createResetEquation; | ||
| 1506 | |||
| 1507 | // ============================================================ | ||
| 1508 | // Expression substitution helpers | ||
| 1509 | // ============================================================ | ||
| 1510 | |||
| 1511 | protected | ||
| 1512 | function subsActiveStateInEq | ||
| 1513 | "Replace activeState(x) → x.active in all expressions of an equation." | ||
| 1514 | input output Equation eq; | ||
| 1515 | algorithm | ||
| 1516 | 91 | eq := Equation.mapExp(eq, subsActiveStateInExp); | |
| 1517 | end subsActiveStateInEq; | ||
| 1518 | |||
| 1519 | protected | ||
| 1520 | function subsActiveStateInExp | ||
| 1521 | "Replace activeState(x) → x.active in an expression." | ||
| 1522 | input output Expression exp; | ||
| 1523 | algorithm | ||
| 1524 | 182 | exp := Expression.map(exp, subsActiveStateHelper); | |
| 1525 | end subsActiveStateInExp; | ||
| 1526 | |||
| 1527 | protected | ||
| 1528 | function subsActiveStateHelper | ||
| 1529 | input output Expression exp; | ||
| 1530 | protected | ||
| 1531 | Call expCall; | ||
| 1532 | ComponentRef argCref; | ||
| 1533 | Expression newExp; | ||
| 1534 | algorithm | ||
| 1535 | try | ||
| 1536 |
2/2✓ Branch 0 taken 622 times.
✓ Branch 1 taken 78 times.
|
700 | Expression.CALL(call = expCall) := exp; |
| 1537 |
1/4✗ Branch 1 not taken.
✓ Branch 2 taken 78 times.
✗ Branch 5 not taken.
✗ Branch 6 not taken.
|
78 | if not stringEq(Call.functionNameLast(expCall), "activeState") then fail(); end if; |
| 1538 | ✗ | {Expression.CREF(cref = argCref)} := Call.arguments(expCall); | |
| 1539 | ✗ | newExp := makeCrefExp(qCref("active", Type.BOOLEAN(), {}, argCref), Type.BOOLEAN()); | |
| 1540 | exp := newExp; | ||
| 1541 | else | ||
| 1542 | end try; | ||
| 1543 | end subsActiveStateHelper; | ||
| 1544 | |||
| 1545 | protected | ||
| 1546 | function subsPreviousCrefs | ||
| 1547 | "Replace previous(x) → x_previous for x in stateVarCrefs." | ||
| 1548 | input output Expression exp; | ||
| 1549 | input list<ComponentRef> stateVarCrefs; | ||
| 1550 | input output Boolean found; | ||
| 1551 | protected | ||
| 1552 | list<Expression> args; | ||
| 1553 | Expression arg1; | ||
| 1554 | Type argTy; | ||
| 1555 | ComponentRef argCref; | ||
| 1556 | Call expCall; | ||
| 1557 | Expression newExp; | ||
| 1558 | algorithm | ||
| 1559 | try | ||
| 1560 |
2/2✓ Branch 0 taken 12 times.
✓ Branch 1 taken 4 times.
|
16 | Expression.CALL(call = expCall) := exp; |
| 1561 |
2/4✓ Branch 1 taken 4 times.
✗ Branch 2 not taken.
✗ Branch 5 not taken.
✓ Branch 6 taken 4 times.
|
4 | if not stringEq(Call.functionNameLast(expCall), "previous") then fail(); end if; |
| 1562 | 4 | args := Call.arguments(expCall); | |
| 1563 |
1/2✗ Branch 1 not taken.
✓ Branch 2 taken 4 times.
|
4 | if listLength(args) <> 1 then fail(); end if; |
| 1564 | 4 | arg1 := listHead(args); | |
| 1565 |
1/2✗ Branch 0 not taken.
✓ Branch 1 taken 4 times.
|
4 | Expression.CREF(ty = argTy, cref = argCref) := arg1; |
| 1566 |
1/2✗ Branch 0 not taken.
✓ Branch 1 taken 4 times.
|
4 | for svc in stateVarCrefs loop |
| 1567 | ✗ | if ComponentRef.isEqual(svc, argCref) then | |
| 1568 | ✗ | newExp := makeCrefExp( | |
| 1569 | ComponentRef.prefixCref( | ||
| 1570 | InstNode.NAME_NODE(ComponentRef.firstName(argCref) + "_previous"), | ||
| 1571 | argTy, {}, | ||
| 1572 | ComponentRef.rest(argCref)), | ||
| 1573 | argTy); | ||
| 1574 | exp := newExp; | ||
| 1575 | found := true; | ||
| 1576 | break; | ||
| 1577 | end if; | ||
| 1578 | end for; | ||
| 1579 | else | ||
| 1580 | end try; | ||
| 1581 | end subsPreviousCrefs; | ||
| 1582 | |||
| 1583 | // ============================================================ | ||
| 1584 | // createTandC | ||
| 1585 | // ============================================================ | ||
| 1586 | |||
| 1587 | protected | ||
| 1588 | function createTandC | ||
| 1589 | "Build the sorted transition list (t) and condition list (c) from transition NORETCALL equations." | ||
| 1590 | input list<ComponentRef> stateCrefs; | ||
| 1591 | input list<Equation> transitionEqs; | ||
| 1592 | output list<Transition> t; | ||
| 1593 | output list<Expression> c; | ||
| 1594 | protected | ||
| 1595 | list<Transition> transitions; | ||
| 1596 | algorithm | ||
| 1597 | 3 | transitions := List.filterMap(transitionEqs, | |
| 1598 | function extractTransition(stateCrefs = stateCrefs)); | ||
| 1599 | 3 | t := List.sort(transitions, priorityGt); | |
| 1600 |
5/6✓ Branch 0 taken 5 times.
✓ Branch 1 taken 3 times.
✓ Branch 2 taken 5 times.
✓ Branch 3 taken 3 times.
✓ Branch 5 taken 3 times.
✗ Branch 6 not taken.
|
8 | c := list(tr.condition for tr in t); |
| 1601 | end createTandC; | ||
| 1602 | |||
| 1603 | protected | ||
| 1604 | function extractTransition | ||
| 1605 | "Extract a Transition record from a transition() NORETCALL equation. Fails if not a transition." | ||
| 1606 | input Equation eq; | ||
| 1607 | input list<ComponentRef> stateCrefs; | ||
| 1608 | output Transition trans; | ||
| 1609 | protected | ||
| 1610 | ComponentRef crFrom, crTo; | ||
| 1611 | Expression cond; | ||
| 1612 | Boolean imm = true, rst = true, syn = false; | ||
| 1613 | Integer prio = 1; | ||
| 1614 | Integer from, to; | ||
| 1615 | list<Expression> args; | ||
| 1616 | Call eqCall; | ||
| 1617 | algorithm | ||
| 1618 |
2/4✗ Branch 0 not taken.
✓ Branch 1 taken 5 times.
✗ Branch 3 not taken.
✓ Branch 4 taken 5 times.
|
5 | Equation.NORETCALL(exp = Expression.CALL(call = eqCall)) := eq; |
| 1619 |
2/4✓ Branch 1 taken 5 times.
✗ Branch 2 not taken.
✗ Branch 5 not taken.
✓ Branch 6 taken 5 times.
|
5 | if not stringEq(Call.functionNameLast(eqCall), "transition") then fail(); end if; |
| 1620 | 5 | args := Call.arguments(eqCall); | |
| 1621 |
1/2✗ Branch 1 not taken.
✓ Branch 2 taken 5 times.
|
5 | Expression.CREF(cref = crFrom) := listGet(args, 1); |
| 1622 |
1/2✗ Branch 1 not taken.
✓ Branch 2 taken 5 times.
|
5 | Expression.CREF(cref = crTo) := listGet(args, 2); |
| 1623 | 5 | cond := listGet(args, 3); | |
| 1624 |
2/4✓ Branch 1 taken 5 times.
✗ Branch 2 not taken.
✗ Branch 4 not taken.
✓ Branch 5 taken 5 times.
|
5 | if listLength(args) >= 4 then Expression.BOOLEAN(value = imm) := listGet(args, 4); end if; |
| 1625 |
2/4✓ Branch 1 taken 5 times.
✗ Branch 2 not taken.
✗ Branch 4 not taken.
✓ Branch 5 taken 5 times.
|
5 | if listLength(args) >= 5 then Expression.BOOLEAN(value = rst) := listGet(args, 5); end if; |
| 1626 |
2/4✓ Branch 1 taken 5 times.
✗ Branch 2 not taken.
✗ Branch 4 not taken.
✓ Branch 5 taken 5 times.
|
5 | if listLength(args) >= 6 then Expression.BOOLEAN(value = syn) := listGet(args, 6); end if; |
| 1627 |
2/4✓ Branch 1 taken 5 times.
✗ Branch 2 not taken.
✗ Branch 4 not taken.
✓ Branch 5 taken 5 times.
|
5 | if listLength(args) >= 7 then Expression.INTEGER(value = prio) := listGet(args, 7); end if; |
| 1628 | from := 1; | ||
| 1629 |
1/2✓ Branch 0 taken 7 times.
✗ Branch 1 not taken.
|
7 | for sc in stateCrefs loop |
| 1630 |
2/2✓ Branch 1 taken 2 times.
✓ Branch 2 taken 5 times.
|
7 | if ComponentRef.isEqual(sc, crFrom) then break; end if; |
| 1631 | 2 | from := from + 1; | |
| 1632 | end for; | ||
| 1633 | to := 1; | ||
| 1634 |
1/2✓ Branch 0 taken 8 times.
✗ Branch 1 not taken.
|
8 | for sc in stateCrefs loop |
| 1635 |
2/2✓ Branch 1 taken 3 times.
✓ Branch 2 taken 5 times.
|
8 | if ComponentRef.isEqual(sc, crTo) then break; end if; |
| 1636 | 3 | to := to + 1; | |
| 1637 | end for; | ||
| 1638 |
3/6✓ Branch 0 taken 5 times.
✗ Branch 1 not taken.
✗ Branch 2 not taken.
✓ Branch 3 taken 5 times.
✓ Branch 4 taken 5 times.
✗ Branch 5 not taken.
|
15 | trans := TRANSITION(from, to, cond, imm, rst, syn, prio); |
| 1639 | end extractTransition; | ||
| 1640 | |||
| 1641 | protected | ||
| 1642 | function priorityGt | ||
| 1643 | "Greater-than comparator for List.sort: compare(a,b)=true means b comes before a. | ||
| 1644 | Lower priority numbers (= higher MLS priority) sort first." | ||
| 1645 | input Transition t1; | ||
| 1646 | input Transition t2; | ||
| 1647 | output Boolean gt; | ||
| 1648 | algorithm | ||
| 1649 | 2 | gt := t1.priority > t2.priority; | |
| 1650 | end priorityGt; | ||
| 1651 | |||
| 1652 | // ============================================================ | ||
| 1653 | // Predicate helpers | ||
| 1654 | // ============================================================ | ||
| 1655 | |||
| 1656 | protected | ||
| 1657 | function isTransitionOrInitialState | ||
| 1658 | "True if the equation is a transition() or initialState() NORETCALL." | ||
| 1659 | input Equation eq; | ||
| 1660 | output Boolean res = false; | ||
| 1661 | algorithm | ||
| 1662 | () := match eq | ||
| 1663 | local | ||
| 1664 | Call eqCall; | ||
| 1665 | case Equation.NORETCALL(exp = Expression.CALL(call = eqCall)) | ||
| 1666 | algorithm | ||
| 1667 | res := match Call.functionNameLast(eqCall) | ||
| 1668 | case "transition" then true; | ||
| 1669 | case "initialState" then true; | ||
| 1670 | else false; | ||
| 1671 | end match; | ||
| 1672 | then (); | ||
| 1673 | else (); | ||
| 1674 | end match; | ||
| 1675 | end isTransitionOrInitialState; | ||
| 1676 | |||
| 1677 | protected | ||
| 1678 | function isTransitionForGroup | ||
| 1679 | "True if the equation is a transition() involving states in stateCrefs." | ||
| 1680 | input Equation eq; | ||
| 1681 | input list<ComponentRef> stateCrefs; | ||
| 1682 | output Boolean res = false; | ||
| 1683 | protected | ||
| 1684 | ComponentRef cr; | ||
| 1685 | algorithm | ||
| 1686 | () := match eq | ||
| 1687 | local | ||
| 1688 | Call eqCall; | ||
| 1689 | case Equation.NORETCALL(exp = Expression.CALL(call = eqCall)) | ||
| 1690 | guard stringEq(Call.functionNameLast(eqCall), "transition") | ||
| 1691 | algorithm | ||
| 1692 |
1/2✗ Branch 2 not taken.
✓ Branch 3 taken 5 times.
|
5 | Expression.CREF(cref = cr) := listHead(Call.arguments(eqCall)); |
| 1693 |
1/2✓ Branch 0 taken 7 times.
✗ Branch 1 not taken.
|
7 | for sc in stateCrefs loop |
| 1694 |
2/2✓ Branch 1 taken 2 times.
✓ Branch 2 taken 5 times.
|
7 | if ComponentRef.isEqual(cr, sc) then res := true; break; end if; |
| 1695 | end for; | ||
| 1696 | then (); | ||
| 1697 | else (); | ||
| 1698 | end match; | ||
| 1699 | end isTransitionForGroup; | ||
| 1700 | |||
| 1701 | protected | ||
| 1702 | function isInitialStateForGroup | ||
| 1703 | "True if the equation is the initialState() for the given init state." | ||
| 1704 | input Equation eq; | ||
| 1705 | input ComponentRef initStateCref; | ||
| 1706 | output Boolean res = false; | ||
| 1707 | protected | ||
| 1708 | ComponentRef cr; | ||
| 1709 | algorithm | ||
| 1710 | () := match eq | ||
| 1711 | local | ||
| 1712 | Call eqCall; | ||
| 1713 | case Equation.NORETCALL(exp = Expression.CALL(call = eqCall)) | ||
| 1714 | guard stringEq(Call.functionNameLast(eqCall), "initialState") | ||
| 1715 | algorithm | ||
| 1716 |
1/2✗ Branch 2 not taken.
✓ Branch 3 taken 3 times.
|
3 | Expression.CREF(cref = cr) := listHead(Call.arguments(eqCall)); |
| 1717 | 3 | res := ComponentRef.isEqual(cr, initStateCref); | |
| 1718 | then (); | ||
| 1719 | else (); | ||
| 1720 | end match; | ||
| 1721 | end isInitialStateForGroup; | ||
| 1722 | |||
| 1723 | protected | ||
| 1724 | function isEquationOfState | ||
| 1725 | "True if the equation belongs to state component stateCref. | ||
| 1726 | Uses the equation's instantiation scope to avoid ambiguity: | ||
| 1727 | an equation 'a.y = ...' with scope='c' belongs to state 'a.c' (inner SM), | ||
| 1728 | not to state 'a' (outer SM), even though 'a.y' has 'a' as a prefix." | ||
| 1729 | input Equation eq; | ||
| 1730 | input ComponentRef stateCref; | ||
| 1731 | output Boolean res = false; | ||
| 1732 | protected | ||
| 1733 | NFInstNode.ScopeRef eqScope; | ||
| 1734 | String stateName; | ||
| 1735 | algorithm | ||
| 1736 | 24 | stateName := ComponentRef.firstName(stateCref); | |
| 1737 | () := match eq | ||
| 1738 | case Equation.EQUALITY(scope = eqScope) | ||
| 1739 | algorithm | ||
| 1740 |
3/4✓ Branch 2 taken 8 times.
✗ Branch 3 not taken.
✓ Branch 7 taken 4 times.
✓ Branch 8 taken 4 times.
|
8 | res := stringEqual(InstNode.name(InstNode.fromCell(eqScope)), stateName); |
| 1741 | then (); | ||
| 1742 | case Equation.WHEN(scope = eqScope) | ||
| 1743 | algorithm | ||
| 1744 | ✗ | res := stringEqual(InstNode.name(InstNode.fromCell(eqScope)), stateName); | |
| 1745 | then (); | ||
| 1746 | else (); | ||
| 1747 | end match; | ||
| 1748 | end isEquationOfState; | ||
| 1749 | |||
| 1750 | protected | ||
| 1751 | function isVariableOfState | ||
| 1752 | "True if the variable name has stateCref as its outer prefix." | ||
| 1753 | input Variable var; | ||
| 1754 | input ComponentRef stateCref; | ||
| 1755 | output Boolean res; | ||
| 1756 | algorithm | ||
| 1757 | 4 | res := crefHasPrefix(stateCref, var.name); | |
| 1758 | end isVariableOfState; | ||
| 1759 | |||
| 1760 | protected | ||
| 1761 | function isOuterStateEquation | ||
| 1762 | "True if the equation is an outer-output equation from ANY state in stateCrefs. | ||
| 1763 | These are equations whose scope matches a state component name but whose LHS is the outer variable." | ||
| 1764 | input Equation eq; | ||
| 1765 | input list<ComponentRef> stateCrefs; | ||
| 1766 | output Boolean res = false; | ||
| 1767 | protected | ||
| 1768 | NFInstNode.ScopeRef eqScope; | ||
| 1769 | String scopeName; | ||
| 1770 | algorithm | ||
| 1771 | () := match eq | ||
| 1772 | case Equation.EQUALITY(scope = eqScope) | ||
| 1773 | algorithm | ||
| 1774 | 4 | scopeName := InstNode.name(InstNode.fromCell(eqScope)); | |
| 1775 |
1/2✓ Branch 0 taken 6 times.
✗ Branch 1 not taken.
|
6 | for stateCref in stateCrefs loop |
| 1776 |
3/4✓ Branch 1 taken 6 times.
✗ Branch 2 not taken.
✓ Branch 5 taken 4 times.
✓ Branch 6 taken 2 times.
|
6 | if stringEqual(scopeName, ComponentRef.firstName(stateCref)) then |
| 1777 | res := true; | ||
| 1778 | 4 | return; | |
| 1779 | end if; | ||
| 1780 | end for; | ||
| 1781 | then (); | ||
| 1782 | case Equation.WHEN(scope = eqScope) | ||
| 1783 | algorithm | ||
| 1784 | ✗ | scopeName := InstNode.name(InstNode.fromCell(eqScope)); | |
| 1785 | ✗ | for stateCref in stateCrefs loop | |
| 1786 | ✗ | if stringEqual(scopeName, ComponentRef.firstName(stateCref)) then | |
| 1787 | res := true; | ||
| 1788 | ✗ | return; | |
| 1789 | end if; | ||
| 1790 | end for; | ||
| 1791 | then (); | ||
| 1792 | else (); | ||
| 1793 | end match; | ||
| 1794 | end isOuterStateEquation; | ||
| 1795 | |||
| 1796 | protected | ||
| 1797 | function generateMergeEquation | ||
| 1798 | "Generate merge equation for an outer variable written by state components. | ||
| 1799 | Result: x = if state1.active then state1.x else if state2.active then state2.x else previous(x)" | ||
| 1800 | input ComponentRef outerVarCref; | ||
| 1801 | input UnorderedMap<ComponentRef, list<tuple<ComponentRef, ComponentRef>>> outerVarMap; | ||
| 1802 | input list<Variable> allVariables; | ||
| 1803 | input output list<Equation> accEqs; | ||
| 1804 | input output list<Variable> accVars; | ||
| 1805 | protected | ||
| 1806 | list<tuple<ComponentRef, ComponentRef>> stateEntries; | ||
| 1807 | Expression mergeRhs, outerVarExp; | ||
| 1808 | Type ty; | ||
| 1809 | ComponentRef activeRef, perStateVarRef; | ||
| 1810 | DAE.ElementSource src; | ||
| 1811 | algorithm | ||
| 1812 | 2 | stateEntries := UnorderedMap.getOrDefault(outerVarCref, outerVarMap, {}); | |
| 1813 |
1/2✓ Branch 0 taken 2 times.
✗ Branch 1 not taken.
|
2 | if listEmpty(stateEntries) then |
| 1814 | ✗ | return; | |
| 1815 | end if; | ||
| 1816 | |||
| 1817 | // Determine type from the outer variable | ||
| 1818 | ty := Type.INTEGER(); // default | ||
| 1819 |
1/2✓ Branch 0 taken 2 times.
✗ Branch 1 not taken.
|
2 | for v in allVariables loop |
| 1820 |
1/2✓ Branch 1 taken 2 times.
✗ Branch 2 not taken.
|
2 | if ComponentRef.isEqual(v.name, outerVarCref) then |
| 1821 | 2 | ty := v.ty; | |
| 1822 | 2 | break; | |
| 1823 | end if; | ||
| 1824 | end for; | ||
| 1825 | 2 | outerVarExp := makeCrefExp(outerVarCref, ty); | |
| 1826 | |||
| 1827 | // Build merge rhs: if state1.active then state1.x else if state2.active then state2.x else previous(x) | ||
| 1828 | // stateEntries is in reverse order (last state processed first), so build from the end | ||
| 1829 | 2 | mergeRhs := makePreviousCall(outerVarExp, ty); | |
| 1830 |
2/2✓ Branch 0 taken 4 times.
✓ Branch 1 taken 2 times.
|
6 | for entry in stateEntries loop |
| 1831 | 4 | (activeRef, perStateVarRef) := entry; | |
| 1832 | 4 | mergeRhs := makeIfExp( | |
| 1833 | makeCrefExp(activeRef, Type.BOOLEAN()), | ||
| 1834 | makeCrefExp(perStateVarRef, ty), | ||
| 1835 | mergeRhs, ty); | ||
| 1836 | end for; | ||
| 1837 | |||
| 1838 | 2 | src := ElementSource.createElementSource(Absyn.dummyInfo); | |
| 1839 | 2 | accEqs := Equation.EQUALITY(outerVarExp, mergeRhs, ty, NFInstNode.NO_SCOPE, src, ScalarizeMode.NO_PREFERENCE) :: accEqs; | |
| 1840 | end generateMergeEquation; | ||
| 1841 | |||
| 1842 | // ============================================================ | ||
| 1843 | // ComponentRef utilities | ||
| 1844 | // ============================================================ | ||
| 1845 | |||
| 1846 | protected | ||
| 1847 | function qCref | ||
| 1848 | "Build a qualified ComponentRef: prefix.name[subs]" | ||
| 1849 | input String name; | ||
| 1850 | input Type ty; | ||
| 1851 | input list<Subscript> subs; | ||
| 1852 | input ComponentRef prefixCr; | ||
| 1853 | output ComponentRef cref; | ||
| 1854 | algorithm | ||
| 1855 | 205 | cref := ComponentRef.fromNode(InstNode.NAME_NODE(name), ty, subs); | |
| 1856 | 205 | cref := ComponentRef.prepend(prefixCr, cref); | |
| 1857 | end qCref; | ||
| 1858 | |||
| 1859 | protected | ||
| 1860 | function makeSMSPrefix | ||
| 1861 | "Build the 'smOf.initStateName' prefix for SMS variables." | ||
| 1862 | input ComponentRef initStateCref; | ||
| 1863 | output ComponentRef preRef; | ||
| 1864 | algorithm | ||
| 1865 | 42 | preRef := ComponentRef.fromNode(InstNode.NAME_NODE(SMS_PRE), Type.UNKNOWN(), {}); | |
| 1866 | 42 | preRef := ComponentRef.append(initStateCref, preRef); | |
| 1867 | end makeSMSPrefix; | ||
| 1868 | |||
| 1869 | // ============================================================ | ||
| 1870 | // Variable creation helpers | ||
| 1871 | // ============================================================ | ||
| 1872 | |||
| 1873 | protected | ||
| 1874 | function makeVar | ||
| 1875 | "Create a synthetic discrete Variable." | ||
| 1876 | input ComponentRef name; | ||
| 1877 | input Type ty; | ||
| 1878 | input Variability var; | ||
| 1879 | output Variable v; | ||
| 1880 | protected | ||
| 1881 | Attributes attr; | ||
| 1882 | algorithm | ||
| 1883 | attr := NFAttributes.DEFAULT_ATTR; | ||
| 1884 | 122 | attr.variability := var; | |
| 1885 | 122 | v := Variable.VARIABLE(name, ty, NFBinding.EMPTY_BINDING, Visibility.PUBLIC, | |
| 1886 | attr, {}, {}, SCode.COMMENT(NONE(), NONE()), Absyn.dummyInfo, | ||
| 1887 | NFBackendExtension.DUMMY_BACKEND_INFO); | ||
| 1888 | end makeVar; | ||
| 1889 | |||
| 1890 | protected | ||
| 1891 | function makeVarWithStart | ||
| 1892 | "Create a synthetic discrete Variable with a fixed start value." | ||
| 1893 | input ComponentRef name; | ||
| 1894 | input Type ty; | ||
| 1895 | input Variability var; | ||
| 1896 | input Expression startExp; | ||
| 1897 | output Variable v; | ||
| 1898 | algorithm | ||
| 1899 | 48 | v := makeVar(name, ty, var); | |
| 1900 | 48 | v.typeAttributes := { | |
| 1901 | ("start", Binding.makeFlat(startExp, Variability.CONSTANT, NFBinding.Source.GENERATED)), | ||
| 1902 | ("fixed", Binding.makeFlat(Expression.BOOLEAN(true), Variability.CONSTANT, NFBinding.Source.GENERATED)) | ||
| 1903 | }; | ||
| 1904 | end makeVarWithStart; | ||
| 1905 | |||
| 1906 | protected | ||
| 1907 | function makeVarWithBinding | ||
| 1908 | "Create a synthetic parameter Variable with a binding expression." | ||
| 1909 | input ComponentRef name; | ||
| 1910 | input Type ty; | ||
| 1911 | input Variability var; | ||
| 1912 | input Expression bindExp; | ||
| 1913 | output Variable v; | ||
| 1914 | algorithm | ||
| 1915 | 33 | v := makeVar(name, ty, var); | |
| 1916 | 33 | v.binding := Binding.makeFlat(bindExp, var, NFBinding.Source.GENERATED); | |
| 1917 | end makeVarWithBinding; | ||
| 1918 | |||
| 1919 | // ============================================================ | ||
| 1920 | // Equation creation helpers | ||
| 1921 | // ============================================================ | ||
| 1922 | |||
| 1923 | protected | ||
| 1924 | function makeEq | ||
| 1925 | "Create a simple equality equation." | ||
| 1926 | input Expression lhs; | ||
| 1927 | input Expression rhs; | ||
| 1928 | input Type ty; | ||
| 1929 | output Equation eq; | ||
| 1930 | algorithm | ||
| 1931 | 85 | eq := Equation.EQUALITY(lhs, rhs, ty, NFInstNode.NO_SCOPE, DAE.emptyElementSource, ScalarizeMode.NO_PREFERENCE); | |
| 1932 | end makeEq; | ||
| 1933 | |||
| 1934 | // ============================================================ | ||
| 1935 | // Expression creation helpers | ||
| 1936 | // ============================================================ | ||
| 1937 | |||
| 1938 | protected | ||
| 1939 | function makeCrefExp | ||
| 1940 | "Create Expression.CREF from a ComponentRef." | ||
| 1941 | input ComponentRef cref; | ||
| 1942 | input Type ty; | ||
| 1943 | output Expression exp; | ||
| 1944 | algorithm | ||
| 1945 | 281 | exp := Expression.CREF(ty, cref); | |
| 1946 | end makeCrefExp; | ||
| 1947 | |||
| 1948 | protected | ||
| 1949 | function makeIfExp | ||
| 1950 | "Create an IF expression." | ||
| 1951 | input Expression cond; | ||
| 1952 | input Expression thenExp; | ||
| 1953 | input Expression elseExp; | ||
| 1954 | input Type ty; | ||
| 1955 | output Expression exp; | ||
| 1956 | algorithm | ||
| 1957 | 88 | exp := Expression.IF(ty, cond, thenExp, elseExp); | |
| 1958 | end makeIfExp; | ||
| 1959 | |||
| 1960 | protected | ||
| 1961 | function makePreviousCall | ||
| 1962 | "Create pre(exp) for DT state machine semantics." | ||
| 1963 | input Expression exp; | ||
| 1964 | input Type ty; | ||
| 1965 | output Expression result; | ||
| 1966 | algorithm | ||
| 1967 | 112 | result := Expression.CALL(Call.makeTypedCall( | |
| 1968 | NFBuiltinFuncs.PREVIOUS, {exp}, Variability.DISCRETE, Purity.IMPURE, ty)); | ||
| 1969 | end makePreviousCall; | ||
| 1970 | |||
| 1971 | function makeInitialCall | ||
| 1972 | "Create initial() expression — true during initialization phase." | ||
| 1973 | output Expression result; | ||
| 1974 | algorithm | ||
| 1975 | ✗ | result := Expression.CALL(Call.makeTypedCall( | |
| 1976 | NFBuiltinFuncs.INITIAL, {}, Variability.DISCRETE, Purity.IMPURE, Type.BOOLEAN())); | ||
| 1977 | end makeInitialCall; | ||
| 1978 | |||
| 1979 | protected | ||
| 1980 | function makeMaxIntArrCall | ||
| 1981 | "Create max({e1, e2, ...}) for an integer array." | ||
| 1982 | input list<Expression> exps; | ||
| 1983 | output Expression result; | ||
| 1984 | protected | ||
| 1985 | Type arrTy; | ||
| 1986 | algorithm | ||
| 1987 | 12 | arrTy := Type.ARRAY(Type.INTEGER(), {Dimension.INTEGER(listLength(exps), Variability.STRUCTURAL_PARAMETER)}); | |
| 1988 | 12 | result := Expression.CALL(Call.makeTypedCall( | |
| 1989 | NFBuiltinFuncs.MAX_INT_ARR, | ||
| 1990 | {Expression.ARRAY(arrTy, listArray(exps), true)}, | ||
| 1991 | Variability.DISCRETE, Purity.PURE, Type.INTEGER())); | ||
| 1992 | end makeMaxIntArrCall; | ||
| 1993 | |||
| 1994 | protected | ||
| 1995 | function makeSampleTimeCall | ||
| 1996 | "Create sample(time, Clock()) with an inferred clock for time-related SM equations. | ||
| 1997 | The sample() call is needed so the backend detects a clocked partition." | ||
| 1998 | output Expression result; | ||
| 1999 | protected | ||
| 2000 | Expression timeExp, clockExp; | ||
| 2001 | Type ty; | ||
| 2002 | algorithm | ||
| 2003 | ty := Type.REAL(); | ||
| 2004 | 12 | timeExp := Expression.CREF(ty, | |
| 2005 | ComponentRef.prefixCref(InstNode.NAME_NODE("time"), ty, {}, ComponentRef.EMPTY())); | ||
| 2006 | 12 | clockExp := Expression.CLKCONST(Expression.ClockKind.INFERRED_CLOCK(System.tmpTickIndex(Global.inferredClock_index))); | |
| 2007 | 24 | result := Expression.CALL(Call.makeTypedCall( | |
| 2008 | NFBuiltinFuncs.SAMPLE_CLOCKED, {timeExp, clockExp}, | ||
| 2009 | Variability.CONTINUOUS, Purity.IMPURE, ty)); | ||
| 2010 | end makeSampleTimeCall; | ||
| 2011 | |||
| 2012 | protected | ||
| 2013 | function makeRelationEq | ||
| 2014 | "Create exp1 == exp2." | ||
| 2015 | input Expression exp1; | ||
| 2016 | input Expression exp2; | ||
| 2017 | input Type ty; | ||
| 2018 | output Expression result; | ||
| 2019 | algorithm | ||
| 2020 | 45 | result := Expression.RELATION(exp1, Operator.makeEqual(ty), exp2, 0); | |
| 2021 | end makeRelationEq; | ||
| 2022 | |||
| 2023 | protected | ||
| 2024 | function makeRelationGt | ||
| 2025 | "Create exp1 > exp2." | ||
| 2026 | input Expression exp1; | ||
| 2027 | input Expression exp2; | ||
| 2028 | input Type ty; | ||
| 2029 | output Expression result; | ||
| 2030 | algorithm | ||
| 2031 | 6 | result := Expression.RELATION(exp1, Operator.makeGreater(ty), exp2, 0); | |
| 2032 | end makeRelationGt; | ||
| 2033 | |||
| 2034 | // ============================================================ | ||
| 2035 | // Start value helpers | ||
| 2036 | // ============================================================ | ||
| 2037 | |||
| 2038 | protected | ||
| 2039 | function getStartValue | ||
| 2040 | "Extract start Expression from a Variable; fall back to a type default." | ||
| 2041 | input Variable var; | ||
| 2042 | output Expression startExp; | ||
| 2043 | protected | ||
| 2044 | String attrName; | ||
| 2045 | Binding attrBinding; | ||
| 2046 | Option<Expression> startOpt; | ||
| 2047 | Type ty; | ||
| 2048 | algorithm | ||
| 2049 | ✗ | for attr in var.typeAttributes loop | |
| 2050 | ✗ | (attrName, attrBinding) := attr; | |
| 2051 | ✗ | if attrName == "start" then | |
| 2052 | ✗ | startOpt := Binding.typedExp(attrBinding); | |
| 2053 | ✗ | if isSome(startOpt) then | |
| 2054 | ✗ | SOME(startExp) := startOpt; | |
| 2055 | ✗ | return; | |
| 2056 | end if; | ||
| 2057 | end if; | ||
| 2058 | end for; | ||
| 2059 | // Fall back to type default | ||
| 2060 | ✗ | ty := var.ty; | |
| 2061 | startExp := match ty | ||
| 2062 | case Type.INTEGER() then Expression.INTEGER(0); | ||
| 2063 | case Type.REAL() then Expression.REAL(0.0); | ||
| 2064 | case Type.BOOLEAN() then Expression.BOOLEAN(false); | ||
| 2065 | case Type.STRING() then Expression.STRING(""); | ||
| 2066 | else Expression.INTEGER(0); | ||
| 2067 | end match; | ||
| 2068 | end getStartValue; | ||
| 2069 | |||
| 2070 | // ============================================================ | ||
| 2071 | // ComponentRef prefix check | ||
| 2072 | // ============================================================ | ||
| 2073 | |||
| 2074 | protected | ||
| 2075 | function crefHasPrefix | ||
| 2076 | "True if the outer scope of cref equals prefix (NF crefs are innermost-first, | ||
| 2077 | so prefix appears at the tail of the cref chain)." | ||
| 2078 | input ComponentRef prefix; | ||
| 2079 | input ComponentRef cref; | ||
| 2080 | output Boolean res = false; | ||
| 2081 | algorithm | ||
| 2082 |
1/2✓ Branch 1 taken 16 times.
✗ Branch 2 not taken.
|
16 | if ComponentRef.isEqual(prefix, cref) then |
| 2083 | res := true; | ||
| 2084 | elseif ComponentRef.isEmpty(cref) then | ||
| 2085 | res := false; | ||
| 2086 | else | ||
| 2087 | 8 | res := crefHasPrefix(prefix, ComponentRef.rest(cref)); | |
| 2088 | end if; | ||
| 2089 | end crefHasPrefix; | ||
| 2090 | |||
| 2091 | annotation(__OpenModelica_Interface="nf_frontend"); | ||
| 2092 | end NFStateMachineFlatten; | ||
| 2093 |