Skip to content

Commit

Permalink
QC fixes
Browse files Browse the repository at this point in the history
  • Loading branch information
nickbattle committed Jan 30, 2024
1 parent c375a11 commit 3566417
Show file tree
Hide file tree
Showing 2 changed files with 13 additions and 2 deletions.
8 changes: 6 additions & 2 deletions fmi3/rule-model/Rules/FmiModelDescription.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -212,7 +212,9 @@ validMinMax(-, evs) == allOf
]
| ev in seq evs & is_NumericKind(kindOf(ev))
]);
])
pre forall ev in seq evs &
is_NumericKind(kindOf(ev)) => ev.min <> nil and ev.max <> nil;
----
// {vdm}
See <<table-type-attributes>>.
Expand Down Expand Up @@ -528,7 +530,9 @@ validClockPriorities(fmd, evs) == allOf
-- ev.name, loc2str(ev.location))
( ev.priority = nil ),
<local> -> true
<local> -> true,
others -> true
end
else
-- @OnFail("%NAME: Clock %s must not have a priority unless SE at %#s",
Expand Down
7 changes: 7 additions & 0 deletions fmi3/rule-model/Rules/ModelVariables.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -328,6 +328,13 @@ validVariableAttributes(sv) ==
eCausality <> <independent>
),
-- @OnFail("%NAME: %s clock causality %s invalid at %#s",
-- sv.name, eCausality, loc2str(sv.location))
(
is_Clock(sv) =>
eCausality in set {<input>, <output>, <local>}
),
-- @OnFail("%NAME: %s initial/variability/start %s/%s/%s invalid at %#s",
-- sv.name, eInitial, eVariability, sv.start, loc2str(sv.location))
(
Expand Down

0 comments on commit 3566417

Please sign in to comment.