Verification Rules

Adding verification shows how a simulation marks each step as passed or failed with CppModel.StepResult. That works for a check at a single step. Many requirements of control system software are about behavior over time instead:

• a valve never leaves its range;
• a high level shuts the valve within 1 s;
• the level settles after a setpoint change, without overshooting too far;
• the modes follow the state machine;
• nothing oscillates, and the actuator doesn't wear itself out.

Verification rules check these. They are part of the library: you create each rule once in your simulation, with its settings, and the library tracks it over time. Use only the rules you need.

• Step rules (Always, Response, Settle, Mode) are updated from the step function with values your code computes.
• Signal rules (Oscillation, Wear, Rate, Energy, Percent) read an output (or input) by name after every step. Your code doesn't call them.

What a rule does to the run

At every step, CppModel.StepResult is the AND of all rules. It is 0 at a step where any rule:

• is violated (a value out of range, an illegal mode change);
• has certainly failed and the failure is still going on (a response past its deadline, energy over budget, a time-in-band share that the rest of the run can no longer reach).

So a failure shows in the CppModel.StepResult graph in the workspace exactly where it happens, and it fails the run, and the program's exit code, like any failed step. If your simulation also sets CppModel.StepResult itself, a failing rule overrides it with 0 for that step; otherwise your value stays.

Each rule also records its own output, CppModel.Verify.<name>: 1 until the rule first fails, then 0 to the end of the run. A failure that lasts only a few steps of a long run stays visible there at any zoom.

When the run ends, every rule's outcome is printed and stored with the execution (see Outcomes).

Writing rules in C

In C, create each rule once in the init function and keep its handle. Update the step rules from the step function. This tank level controller is checked by five step rules and two signal rules:

#include <math.h>
#include <cppmodel/CModel.h>

enum Mode { IDLE = 0, FILL = 1, CONTROL = 2, HIGH = 3 };

static double level, valve;
static int mode;
static CppModelRule_t levelWithinTank, valveShutWhenHigh, highLevelShutsValve, modeSequence, setpointStep;

static void Init(CModelSimulation_ts *self, unsigned long stepTime_ms)
{
    /* ... read parameters, initialize the plant and the controller ... */

    /* Step rules, updated in RunCyclic() */
    levelWithinTank = CppModel_ruleAlways(self, "level within tank", 0.0);
    valveShutWhenHigh = CppModel_ruleAlways(self, "valve shut when high", 0.0);
    highLevelShutsValve = CppModel_ruleResponse(self, "high level shuts valve", 1.0, 0.0); /* within 1 s */
    setpointStep = CppModel_ruleSettle(self, "setpoint step", 0.05, 120.0, 30.0, 0.1);
    modeSequence = CppModel_ruleMode(self, "mode sequence");
    CppModel_modeAllow(modeSequence, IDLE, FILL);
    CppModel_modeAllow(modeSequence, FILL, CONTROL);
    CppModel_modeAllow(modeSequence, CONTROL, HIGH);
    CppModel_modeAllow(modeSequence, HIGH, CONTROL);
    CppModel_modeDwell(modeSequence, FILL, NAN, 300.0); /* fill for at most 300 s */

    /* Signal rules: they read the outputs after every step by themselves */
    CppModel_ruleRate(self, "valve rate", "Tank.Valve", "Tank.Controlling", 50.0);
    CppModel_ruleOscillation(self, "level calm", "Tank.Level", "Tank.Controlling", 0.05, 120.0);
}

void RunCyclic(CModelSimulation_ts *self, unsigned long currentTime_ms)
{
    double setpoint = CppModel_getInputF64(self, "Tank.Setpoint", currentTime_ms < 200000 ? 1.0 : 1.5);

    /* ... run the controller and the tank model ... */

    CppModel_setOutputF64(self, "Tank.Level", level);
    CppModel_setOutputF64(self, "Tank.Valve", valve);
    CppModel_setOutputI32(self, "Tank.Mode", mode);
    CppModel_setOutputU8(self, "Tank.Controlling", mode == CONTROL);

    CppModel_updateAlways(levelWithinTank, CppModel_between(level, 0.0, 2.0));
    CppModel_updateAlways(valveShutWhenHigh,
                          CppModel_implies(CppModel_condition(mode == HIGH), CppModel_atMost(valve, 0.0)));
    CppModel_updateResponse(highLevelShutsValve, level > 1.9, valve == 0.0);
    CppModel_updateMode(modeSequence, mode);
    if (mode != IDLE)
        CppModel_updateSettle(setpointStep, level, setpoint);
}

int main(void)
{
    CModelSimulation_ts *simulation = CppModel_create("TankLevel", 600000, 100);
    if (simulation == NULL)
        return 1;

    CppModel_setInitFunction(simulation, Init);
    CppModel_setRunStepFunction(simulation, RunCyclic);
    CppModel_Simulate(simulation);

    int result = CppModel_getSimulationResult(simulation);
    CppModel_destroy(simulation);

    return result;
}

The simulation doesn't set CppModel.StepResult at all: the rules decide which steps pass, and CppModel_getSimulationResult() fails the run when any rule fails.

CppModel_rulePassed(rule) returns a rule's verdict so far: 1 while it holds, 0 once it has failed. A rule that couldn't be created prints the error and returns NULL; updating NULL does nothing.

Rule	Create	Update
Always	CppModel_ruleAlways(self, name, debounce_s)	CppModel_updateAlways(rule, condition)
Response	CppModel_ruleResponse(self, name, deadline_s, hold_s)	CppModel_updateResponse(rule, trigger, response)
Settle	CppModel_ruleSettle(self, name, band, settleLimit_s, stay_s, overshootLimit)	CppModel_updateSettle(rule, value, target)
Mode	CppModel_ruleMode(self, name), then CppModel_modeAllow(rule, from, to) and CppModel_modeDwell(rule, mode, min_s, max_s)	CppModel_updateMode(rule, mode)
Oscillation	CppModel_ruleOscillation(self, name, signal, active, amplitude, duration_s)	none
Wear	CppModel_ruleWear(self, name, signal, active, maxReversalsPerHour, maxTravelPerHour, deadband)	none
Rate	CppModel_ruleRate(self, name, signal, active, maxRate)	none
Energy	CppModel_ruleEnergy(self, name, signal, active, factor, budget)	none
Percent	CppModel_rulePercent(self, name, signal, active, minPercent)	none

active may be NULL, and NAN means "not checked" for an optional limit.

Writing rules in C++

In C++, the rules are classes in cppmodel::verify. Make each one a member of your simulation, constructed with *this, a name and its settings, and call a step rule like a function in RunCyclic():

#include <cmath>
#include <cppmodel/cppmodel.hpp>

using namespace cppmodel::verify;

class ZoneTest : public cppmodel::Simulation
{
    Always valveRange{*this, "valve range"};
    Always heatNeedsAirflow{*this, "heat needs airflow", 2};          // 2 s debounce
    Response smokeStopsFan{*this, "smoke stops fan", 2, 60};          // within 2 s, then for 60 s
    Settle setpointStep{*this, "setpoint step", 0.5, 1800, 600, 0.8};
    Mode modes{*this, "modes"};
    // Signal rules: nothing to call
    Oscillation calm{*this, "no oscillation", "Zone.Error", 0.15, 1800, "Zone.Running"};
    Energy heating{*this, "heating energy", "P_HEAT_kW", 1.0 / 3600, 15.5}; // kW·s to kWh

public:
    ZoneTest()
    {
        name = "ZoneTest";
        time_ms = 24 * 3600 * 1000;
        stepSize_ms = 1000;

        modes.Allow(OFF, STARTUP).Allow(STARTUP, RUN).Allow(std::nan(""), ALARM) // NaN: from any mode
            .Dwell(STARTUP, std::nan(""), 30);                                   // at most 30 s
    }

    void RunCyclic(unsigned long long time_ms) override
    {
        // ... run the plant and the controller, set the outputs ...
        valveRange(Between(hc, 0, 100));
        heatNeedsAirflow(Implies(hc > 0, fanProof));
        smokeStopsFan(smoke, !fan && hc == 0);
        modes(mode);
        if (occupied)
            setpointStep(T, setpoint);
    }
};

rule.Passed(&margin) gives a rule's verdict so far, and its margin.

For Python and Node.js, see Verification rules in Python and Node.js.

Conditions and margins

Each rule reports a margin in physical units besides pass/fail:

• margin > 0: satisfied, with that much headroom;
• margin < 0: violated by that much.

A margin tells how close a passing run came to failing, and how far a failing one missed. For a condition, the margin is its signed distance, which the condition helpers compute:

C (CModel.h)	C++ (cppmodel::verify)	Holds when	Margin
CppModel_atMost(x, limit)	AtMost(x, limit)	x <= limit	limit - x
CppModel_atLeast(x, limit)	AtLeast(x, limit)	x >= limit	x - limit
CppModel_between(x, low, high)	Between(x, low, high)	low <= x <= high	the lower of the two
CppModel_near(x, target, tol)	Near(x, target, tol)	abs(x - target) <= tol	tol - abs(x - target)
CppModel_and, _or, _not	a && b, a || b, !a		min, max, negated
CppModel_implies(a, b)	Implies(a, b)	!a || b
CppModel_condition(holds)	a bool		none

A plain boolean has no margin. Combined with a condition that has one, it never lends its truth to the other's margin. For example, Implies(mode == RUN, AtMost(valve, 0)) has no margin while the mode isn't RUN.

Rules with time limits report time margins: a response 1.5 s after its trigger, with a 2 s deadline, has a time_s margin of 0.5.

Scope and lifetime

A step rule applies at the steps where your code updates it. To check a rule only while the zone is occupied, update it inside if (occupied). A step without the update doesn't count: an Always violation ends there, and a Settle sees target changes only at steps where it is updated. A time limit that runs out (a response deadline, a settle limit, a maximum dwell) fails its steps whether or not the rule is updated in them.

A signal rule takes an optional active signal: an output that is non-zero while the rule applies. Without one, it applies to the whole run. Record the flags you need as outputs, such as Tank.Controlling above.

A rule lives as long as the simulation, and every run (a persistent simulation runs many) starts it afresh. Creating a rule again under the same name returns the same rule with the new settings. An error is reported (cppmodel::Error in C++, a printed message in C) when a name is already used by another kind of rule, when a step rule is updated outside the step function or twice in one step, or when a rule is given an update of another kind.

Step rules

Always

Always rule{*this, name, debounce_s = 0};   rule(condition);

The condition holds at every step it is updated. A violation counts once it has lasted debounce_s seconds; from then on its steps fail. A shorter one doesn't count, but the margin records that the limit was touched (0).

Use it for invariants (Between(valve, 0, 100)), "never" (!(heating && cooling)), relations between signals (Implies(hc > 0, fanProof), AtLeast(supply, mixed - 0.5)), and guards and latches (Implies(leftAlarm, reset)).

Margin value: the lowest margin of the condition.

Response

Response rule{*this, name, deadline_s, hold_s = 0};   rule(trigger, response);

When trigger becomes true, response must become true within deadline_s seconds and then stay true for hold_s seconds. A trigger that comes while one is still pending is ignored.

Failing steps: every step after the deadline until the response, and the step at which a held response breaks. A trigger too close to the end of the run to judge is reported, not failed.

Margin time_s: the deadline minus the slowest response, or, for a broken hold, the time held minus hold_s.

Chain responses for a required order: a Response from fan to proof within 10 s, then another from proof to mode == RUN within 2 s.

Settle

Settle rule{*this, name, band, settleLimit_s, stay_s, overshootLimit = NaN};   rule(value, target);

When target changes, value must enter target ± band within settleLimit_s and stay there for stay_s. It must not pass the target, in the direction of the change, by more than overshootLimit. A new change ends the previous one; if the value was in band by then, the stay is cut short and still counts.

Failing steps: while the value is late to settle, and while it overshoots beyond the limit.

Margins: time_s, the limit minus the settling time, and overshoot, the limit minus the overshoot.

Metrics: settling time, overshoot and undershoot, and the steady-state error (the mean error while staying in band).

Mode

Mode rule{*this, name};
rule.Allow(from, to);           // NaN: any mode
rule.Dwell(mode, min_s, max_s); // NaN: not checked
rule(mode);                     // every step

Once any transition is allowed, every other change of mode fails its step. Leaving a mode before min_s fails that step, and staying beyond max_s fails each step until the mode changes.

Margin time_s: the lowest dwell margin.

Signal rules

Each signal rule reads an output (or input) named signal after every step. A signal that is never there is an error, which fails the run's last step.

Rule	Checks	Margin	Failing steps
Oscillation	No sustained oscillation larger than amplitude over duration_s	value: limit minus sustained amplitude	While a sustained oscillation is going on
Wear	Direction reversals larger than deadband, and total travel, per hour of active time (NaN: not checked)	reversals_per_h, travel_per_h	From the step where the rest of the run can no longer bring the rate within its limit
Rate	The signal changes by at most maxRate per second	rate	Every step that changes faster than the limit
Energy	The time integral of the signal (per second) times factor stays within budget	energy	From the step the budget is used up
Percent	The signal is non-zero for at least minPercent of the active time	percent	From the step where the rest of the run can no longer reach minPercent

Oscillation measures the signal around its moving mean over duration_s and splits it into half-cycles (crossings beyond ±10 % of the amplitude). It is sustained when the latest half-cycles, at least four and spanning duration_s, all exceed amplitude. A single step change is not an oscillation.

For Percent and Wear, the run's own length is used, so a short failing stretch late in a long run may fail only the last steps.

Outcomes

Each rule's outcome is printed when the run ends:

CppModel.Verify.smoke stops fan: FAIL response 5 s after the trigger at t=7200 s (deadline 2 s); 1 of 1 trigger(s) failed
CppModel.Verify: 14 of 15 rules passed

It is also stored in the execution's verification field, keyed by the rule's name:

"verification": {
  "smoke stops fan": {
    "kind": "response",
    "status": "fail",
    "pass": false,
    "margins": { "time_s": -3.0 },
    "metrics": { "triggers": 1, "answered": 1, "slowest_response_s": 5.0 },
    "violations": [[7202.0, 7205.0]],
    "explanation": "response 5 s after the trigger at t=7200 s (deadline 2 s); 1 of 1 trigger(s) failed"
  }
}

Field	Meaning
status	pass, fail, or error (a signal rule's signal was never there)
margins	Margins by name; {} for a rule without one, null for a margin that isn't finite
violations	Time intervals in seconds; an end that isn't finite is null
metrics	Measured values, per kind of rule

All seven fields are always there. A simulation without rules has no verification field. A local run writes the same field to its results file.

Requirements

A simulation can name the requirements it verifies with CppModel_verifyRequirement(self, id) in C, or VerifyRequirement(id) in C++:

• The whole run: call it in the init function (C++: the constructor or Init()), before any step.
• Some steps: call it in the step function at the steps that exercise the requirement, for example only while the level is high.

static void Init(CModelSimulation_ts *self, unsigned long stepTime_ms)
{
    /* ... */
    CppModel_verifyRequirement(self, "TANK-SAF-001"); /* level limits, checked throughout */
}

void RunCyclic(CModelSimulation_ts *self, unsigned long currentTime_ms)
{
    /* ... */
    if (level > 1.9 || mode == HIGH)
        CppModel_verifyRequirement(self, "TANK-SAF-002"); /* high-level shutdown, exercised only here */
}

When the run ends, the IDs are printed:

CppModel.Requirements: TANK-SAF-001, TANK-SAF-002

The execution records them in its requirements field, with one entry per ID:

"requirements": {
  "TANK-SAF-001": { "whole_run": true, "steps": 0, "from_s": null, "to_s": null },
  "TANK-SAF-002": { "whole_run": false, "steps": 30, "from_s": 412.0, "to_s": 414.9 }
}

They are also written to cppmodel-requirements.json in the working directory, or to the file set in CPPMODEL_REQUIREMENTS_FILE. The file holds one entry per simulation, with its time, passed and the requirements; each run replaces its own simulation's entry and keeps the others. A CI job can collect this file to build a requirement coverage report. Runs that share a working directory and run at the same time can overwrite each other's entries, so give them separate files with CPPMODEL_REQUIREMENTS_FILE.

Naming a requirement says that the test addresses it. Whether it was met is the run's result: passed in the file, and the run's result and CppModel.StepResult in the execution. Only the IDs are recorded; the library doesn't read requirement texts.