Compute time - lgwagner/SpeAR GitHub Wiki

Table of Contents Introduction Inputs Outputs Assumptions Requirements Properties

This component converts the user defied time input on the display into the internal representation in seconds.

These are the input digits at the specific locations on the display (left, middle, right).

The output is the singular time value in seconds

This section informs the model checker of the correct ranges of the input values.

Important Note - You should always take great care when defining an assumption. An assumption limits the constraint space of the model checker. Mistakes may not be immediately discovered since it is completely reliant on user knowledge to give proper reasoning. Limit using assumptions if possible.

This is a simple calculation to change M:SS to seconds only.

This property enforces that the time value is within the acceptable bounds.