Enable JavaScript to interact with content and submit forms on Wolfram websites. Learn how

Wolfram Language & System Documentation Center

SystemModelAlways

SystemModelAlways

SystemModelAlways[t,texpr]

is True if the temporal expression texpr is always True.

SystemModelAlways[t,cond,texpr]

is True if texpr is always True in the intervals where the temporal expression cond is True.

Details

SystemModelAlways is typically used to specify requirements that should always be satisfied, such as always demanding some behavior or always excluding some behavior.
SystemModelAlways[t,texpr[t]] is True if texpr[t] is True for all validation times .

SystemModelAlways[t,texpr[t]] is False if texpr[t] is False for some validation time .

The times and are given by the simulation interval of the system.
The condition cond is often used to select a subset of the validation interval, as in .
SystemModelAlways[t,cond[t],texpr[t]] is True if texpr[t] is True for all t where cond[t] is True.

SystemModelAlways or SystemModelEventually is used as the outer wrapper of a temporal specification in functions like SystemModelValidate.

Examples

open all close all

Basic Examples (1)

Validate the requirement, "In flight, when one engine is off, the air distribution circuit must provide nominal performance.":

Use SystemModelAlways to validate a condition that must always be satisfied:

Scope (4)

Basic Uses (2)

Validate requirements in a model of a pendulum:

Validate the requirement, "The angle must always be between 1 and .":

Validate the numerical solution against the exact result:

Validate the requirement, "The mass of the pendulum must always be to the right of the central position.":

Extract the failure plot:

Validate requirements in a model of a RC circuit:

Validate a requirement with variables evaluated at specific times:

Validate a requirement with variables evaluated at different times:

Condition (2)

Validate requirements for times satisfying conditions in a model of a pendulum:

Validate the requirement, "The angle must always be non-negative for times less than or equal to .":

Validate the requirement, "The angle must always be non-negative for times less than or equal to or a time between and .":

Validate the requirement with a condition that uses intervals instead:

Validate the requirement, "The angle must always be non-negative for times between and .":

Extract the failure plot:

Validate a requirement with a parameter-dependent condition:

Validate a requirement in a model of an RC circuit:

Applications (1)

Start with a simple model of aircraft collision resolution that uses a simple evasion algorithm:

Plot the trajectories of the planes:

Validate the requirement, "The distance between the planes must stay above the distance parameter for each pair of planes.":

The planes happen to get too close. To see this, validate the requirement for all plane distances:

Plot the distance between a couple of planes and the distance threshold:

Top