-
Define a functional constraint for the vending machine component which expresses that each Reset on the service port is followed by a ResetCoinChecker on the coin check port.
-
Define a time constraint (after heading timing constraints) which expresses that a CoinCheckerProblem notification on the coin check port is followed by an OutOfOrder notification on the service port within 2 ms.
-
Run monitoring and inspect the results.