Until Property

Last modified 2014-03-12

Sini

Table of content
  1. Overlapping and Non-overlapping forms
  2. Strong and Weak forms
  3. Until Property Features

table,th,td{border:1px solid black;border-collapse:collapse}

A property is called "until property" if it uses one of the below until operators.

Until properties are categorized as Overlapped & Non-overlapped and Strong & Weak. So overall four different forms of until properties exist.

Weak & Non-Overlappinguntilproperty_expr1 until property_expr2
Strong & Non-Overlappings_untilproperty_expr1 s_until property_expr2
Weak & Overlappinguntil_withproperty_expr1 until_with property_expr2
Strong & Overlappings_until_withproperty_expr1 s_until_with property_expr2

Overlapping and Non-overlapping forms

propertyexpr1 until propertyexpr2 propertyexpr1 suntil propertyexpr2

Non-overlapping form evaluates to true, if propertyexpr1 evaluates to true at every clock tick until one clock tick before propertyexpr2 evaluates to true. Overlapping form evaluates to true, if propertyexpr1 evaluates to true at every clock tick until propertyexpr2 evaluates to true.

propertyexpr1 untilwith propertyexpr2 propertyexpr1 suntilwith propertyexpr2

In both cases, propertyexpr1 evaluation starts from the first clock tick of the evaluation attempt. until_property3

Strong and Weak forms

For strong until property, a current or future clock tick exist at which propertyexpr2 evaluates to true. Weak until property evaluates to true if propertyexpr1 evaluates to true at each clock tick, even if propertyexpr2 never holds.

Until Property Features

Until property typesWeak & Non-overlapping en until out;Strong & Non-overlapping en s_until out;Weak & Overlapping en until out;Strong & Overlapping en s_until out;
The property evaluates to true if 'en' is true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing
until clock tick at which 'out' is true		Yes, But not necessarily including that clock tickYes, But not necessarily including that clock tickYesYes
There exists a current or future clock tick at which 'out' is trueIf not, 'en' should be true for every clock tickYesIf not, 'en' should be true for every clock tickYes
If 'out' is true at the starting clock tick of the evaluation attemppt, then 'en' need not be true at that clock tickYesYesYesYes