temporal

This module provides the basics for defining temporal properties for transition systems.

def G(formula: z3.z3.BoolRef) -> z3.z3.BoolRef:

The globally (G, ☐) temporal operator.

Parameters
  • formula: The formula to apply the globally operator to.
Returns

A formula expressing that the formula holds globally (in all future states).

def F(formula: z3.z3.BoolRef) -> z3.z3.BoolRef:

The eventually (F, ♢) temporal operator.

Parameters
  • formula: The formula to apply the eventually operator to.
Returns

A formula expressing that the formula holds eventually (in some future state).

class Prop(abc.ABC, typing.Generic[T]):

Subclasses of this class represent a temporal property we wish to prove. They must implement the abstract method prop:

class Terminating(Prop[TerminationSystem]):
    def prop(self) -> BoolRef:
        T = Thread("T")
        return F(ForAll(T, Not(self.sys.on(T))))
sys: T

Field holding a reference to the transition system, so that the temporal property can have access to symbols from the signature.

@abstractmethod
def prop(self) -> z3.z3.BoolRef:

Return the temporal property to prove (non-negated).

Returns

Temporal property formula we wish to prove.