Module eqc_temporal

Description
Data Types
Function Index
Function Details

This module provides functions for analysing traces of time-stamped events, to express properties such as that deadlines are met.

Version: 1.46.3

Description

This module provides functions for analysing traces of time-stamped events, to express properties such as that deadlines are met. The analysis is based on an abstract datatype of temporal relations, which represent relations between times in the range 0 to infinity, and arbitrary values. We illustrate how to use the library via a simple example.

Timed Traces of Events

eqc_temporal requires a timed trace of events to analyse--a list of pairs of times (positive integers) and events. For example,

 Trace = [{1,{login,alice,office}},
          {2,{login,bob,home}},
          {8,{login,bob,phone}},
          {10,{send,alice,bob,hello}},
          {11,{logout,alice,office}},
          {20,{deliver,home,hello}},
          {30,{deliver,phone,hello}}].

might represent Alice and Bob using an instant messaging application. Typically events are recorded during the execution of a test case, time-stamped with the time since the start of the test, and then analysed using eqc_temporal after the test has finished.

Building a Temporal Relation

Before a trace can be analysed, it must be converted to a temporal relation using from_timed_list:

 51> Events=eqc_temporal:from_timed_list(Trace).
 [{0,1,[]},
  {1,2,[{login,alice,office}]},
  {2,3,[{login,bob,home}]},
  {3,8,[]},
  {8,9,[{login,bob,phone}]},
  {9,10,[]},
  {10,11,[{send,alice,bob,hello}]},
  {11,12,[{logout,alice,office}]},
  {12,20,[]},
  {20,21,[{deliver,home,hello}]},
  {21,30,[]},
  {30,31,[{deliver,phone,hello}]},
  {31,infinity,[]}]

A temporal relation specifies a set of values related to each time. For example, the third line above says that the relation contains {login,bob,home} at all times between 2 and 3, (not including 3). That is, the relation contains {login,bob,home} at time 2. This relation contains the same information as the list of events, but in a form which is easier to work with.

Note that the representation of temporal relations may change in future versions, so while displaying the representation as diagnostic information is useful, user code should not manipulate temporal relations except using the functions in this module.

Stateful Relations

We often need to track state changes as a result of events. We represent states as a temporal relation too, where an entire set of states can be active at each time. For example, many users can be logged in simultaneously to the instant messaging system. We construct a temporal relation of states using the stateful function:

 4> LoggedIn=eqc_temporal:stateful(
               fun({login,User,Where})->[{User,Where}] end,
               fun({User,Where},{logout,User,Where})->[] end,
               Events).
 [{0,1,[]},
  {1,2,[{alice,office}]},
  {2,8,[{alice,office},{bob,home}]},
  {8,11,[{alice,office},{bob,home},{bob,phone}]},
  {11,infinity,[{bob,home},{bob,phone}]}]

We pass stateful two functions:

One to recognise events that start states--for example, the event {login,User,Where} start the state {User,Where} in the LoggedIn relation,
and one to recognise events that transform states--for example, the event {logout,User,Where} transforms the state {User,Where} into no states (the empty list), terminating the state in the LoggedIn relation.

Both functions return a list of states, since many states can be active simultaneously. Notice that we need only match the interesting cases in these functions... unmatched events are simply ignored.

The relation constructed shows us exactly which users were logged in at each time, and where.

Tracking Messages in Flight

When Alice sends a message to Bob, two messages are actually created, because Bob is logged in both at home and on his phone. (Look at the event trace--it contains two deliveries). To track the messages in flight, we need to combine send events with the logged-in states of the recipients. The product of Events and LoggedIn contains pairs of events and {User,Where} states, which we can use to construct a relation of message lifetimes. We use stateful again to recognise the beginning and end of each message lifetime.

 8> Messages=eqc_temporal:stateful(
               fun({{send,A,B,Msg},{B,Where}})->[{Msg,Where}] end,
               fun({Msg,Where},{{deliver,Where,Msg},{B,Where}})->[] end,
               eqc_temporal:product(Events,LoggedIn)).
 [{0,10,[]},
  {10,21,[{hello,home},{hello,phone}]},
  {21,31,[{hello,phone}]},
  {31,infinity,[]}]

The first function says that when A sends a message to B, who is logged in at Where, then a message to Where is created in the Messages relation. The second function says that this message is deleted again when a matching deliver event occurs. Looking at the result, we can see that {hello,home} was in flight from time 10 to 20, while {hello,phone} was in flight from 10 to 30.

Checking Deadlines

Suppose messages ought to be delivered within 15 time units. We can construct a temporal relation of the overdue messages using all_past, which contains values which have been active for a given period in the past. This effectively shortens the lifetime of each value by the period given.

 9> Overdue=eqc_temporal:all_past(15,Messages).
 [{0,25,[]},{25,31,[{hello,phone}]},{31,infinity,[]}]

Overdue contains all messages which have been in flight throughout the previous 15 time units--and so, are now overdue. In this example, {hello,phone} was overdue between times 25 and 31.

Making a Property

Putting these together, we can write a property that computes the messages that ought to be delivered, and checks that they were delivered in time, in only a few lines of code. We just construct the Overdue relation, and check that it is empty, either via

 Overdue == eqc_temporal:empty()

or via

 eqc_temporal:is_false(Overdue)

(a temporal relation is considered to be false if it contains no values).

A complete property based on this idea might look like this:

 prop_instant_messenger() ->
   ?FORALL(Cmds,commands(?MODULE),
     begin
       start_trace_recording(),
       run_commands(?MODULE,Cmds),
       Trace    = recorded_trace(),
       Events   = from_timed_list(Trace),
       LoggedIn = stateful(
                  fun({login,User,Where})->[{User,Where}] end,
                  fun({User,Where},{logout,User,Where})->[] end,
                  Events),
       Messages = stateful(
                  fun({{send,A,B,Msg},{B,Where}})->[{Msg,Where}] end,
                  fun({Msg,Where},{{deliver,Where,Msg},{B,Where}})->[] end,
                  product(Events,LoggedIn)),
       Overdue  = all_past(15,Messages),
       is_false(Overdue)
     end).

(where start_trace_recording and recorded_trace are assumed to be defined by the user, in any appropriate way). Note that by including the header file

 -include_lib("eqc/include/eqc_temporal.hrl").

then we can import all the eqc_temporal functions automatically.

Tolerating Uncertainty

In the example, the message delivery to Bob's phone missed the deadline, which would cause the property above to fail. Yet in this case, Bob only logged in on his phone just before the original message was sent. In reality, Bob's login might not really be complete, so it may be acceptable for the message to be delivered late--or not at all. Temporal relations can also be used to tolerate this kind of uncertainty, thus avoiding "false positives" during testing. Suppose a login may take up to four time units. Then we can construct

 CertainlyLoggedIn = all_past(4,LoggedIn)

containing those users whose logins are certainly complete. By using CertainlyLoggedIn instead of LoggedIn in the definition of Messages above, we avoid creating the overdue message and thus allow the test to pass.

Data Types

rel()

abstract datatype: rel()

A relation between times and values (arbitrary terms). We say that a value X is true in R at time T, if R relates T to X. A temporal relation R is true at time T if it relates T to some X.

time()

time() = integer()

A non-negative integer.

Function Index

all_future/1	Relate values that will stay true for eternity.
all_future/2	Relate values that will stay true for a given time.
all_past/1	Relate values that have been true since time 0.
all_past/2	Relate values that have been true for a given time.
any_future/1	Relate values that will be true at some point.
any_future/2	Relate values that will become true at some point within the given time.
any_past/1	Relate values that have been true at some point.
any_past/2	Relate values that have been true at some point within the given time.
at/2	Compute the values related to `Time` by `R`.
bind/2	The bind operation of the temporal relation monad.
coarsen/2	Coarsen the resolution of time in a temporal relation, by the factor `K`.
complement/1	The complement of a temporal relation.
completion/1	Turn a temporal relation into a total temporal relation.
constant/1	The constant temporal relation.
domain_size/1	The total time during which a temporal relation is true.
elems/1	Flatten a set valued temporal relation.
empty/0	The empty temporal relation.
filter/2	Filter a temporal relation by a predicate on the range.
flatmap/2	Apply a list valued partial function to the values of a temporal relation.
from_timed_list/1	Construct a temporal relation from a list of time value pairs.
implies/2	Relational implication.
intersection/2	Intersection of two temporal relations.
is_false/1	Check if a temporal relation is empty.
is_subrelation/2	Check if a temporal relation is a subrelation of another temporal relation.
is_true/1	Check if a temporal relation is total.
last/1	Extend a temporal relation to include the most recently related value.
map/2	Apply a (partial) function to the values of a temporal relation.
negation/1	The negation of a temporal relation.
negation/2	The negation of a temporal relation.
partition/2	Partition a temporal relation based on its range.
product/2	The product of two temporal relations.
range/1	The range of a temporal relation.
restrict/2	Restrict a temporal relation to the domain of another temporal relation.
ret/1	A singleton temporal relation.
set/1	Converting a temporal relation to a set valued temporal relation.
shift/2	Shift a temporal relation by a given time.
slice/3	Restrict a temporal relation to a particular time slice.
split_at/2	Split a temporal relation into two temporal relations with disjoint domains.
stateful/3	Apply a simple state machine to a temporal relation.
subtract/2	Subtract one temporal relation from another.
union/2	Union of two temporal relations.
unions/1	Take the union of a list of temporal relations.

Function Details

all_future/1

all_future(R::rel()) -> rel()

Relate values that will stay true for eternity. all_future(R) relates T to X, if R relates T to X for every T' in the range T to infinity.

all_future/2

all_future(Time::time(), R::rel()) -> rel()

Relate values that will stay true for a given time. all_future(Time, R) relates T to X, if R relates T to X for every T' in the range T to T + Time.

all_past/1

all_past(R::rel()) -> rel()

Relate values that have been true since time 0. all_past(R) relates T to X, if R relates T to X for every T' in the range 0 to T.

all_past/2

all_past(Time::time(), R::rel()) -> rel()

Relate values that have been true for a given time. all_past(Time, R) relates T to X, if R relates T to X for every T' in the range T - Time to T.

any_future/1

any_future(R::rel()) -> rel()

Relate values that will be true at some point. any_future(R) relates T to X, if R relates T' to X for some T' >= T. Conceptually equivalent to any_future/2 with an infinite time bound.

any_future/2

any_future(Time::time(), R::rel()) -> rel()

Relate values that will become true at some point within the given time. any_future(Time, R) relates T to X, if R relates T to X for any T' in the range T to T + Time.

any_past/1

any_past(R::rel()) -> rel()

Relate values that have been true at some point. any_past(R) relates T to X, if R relates T' to X for some T' =< T. Conceptually equivalent to any_past/2 with an infinite time bound.

any_past/2

any_past(Time::time(), R::rel()) -> rel()

Relate values that have been true at some point within the given time. any_past(Time, R) relates T to X, if R relates T to X for any T' in the range T - Time to T.

at/2

at(Time::time(), R::rel()) -> [term()]

Compute the values related to Time by R.

bind/2

bind(R::rel(), F::fun((term()) -> rel())) -> rel()

The bind operation of the temporal relation monad. bind(R, F) is the union of shift(T, F(X)) for each X and T such that F(X) is defined and R relates T to X. F can be partial.

coarsen/2

coarsen(K::integer(), R::rel()) -> rel()

Coarsen the resolution of time in a temporal relation, by the factor K. For example, coarsen(1000,R) would convert a temporal relation with times in microseconds to a relation with times in milliseconds.

complement/1

complement(R::rel()) -> rel()

The complement of a temporal relation. complement(R) relates T to X, if X is in the range of R and R does not relate T to X.

completion/1

completion(R::rel()) -> rel()

Equivalent to union(R, negation(R)).

Turn a temporal relation into a total temporal relation.

constant/1

constant(X::term()) -> rel()

The constant temporal relation. constant(X) relates all times to X.

domain_size/1

domain_size(R::rel()) -> time() | infinity

The total time during which a temporal relation is true.

elems/1

elems(R::rel()) -> rel()

Flatten a set valued temporal relation. elems(R) relates T to X, if R relates T to Xs and X is a member of Xs.

empty/0

empty() -> rel()

The empty temporal relation.

filter/2

filter(P::fun((term()) -> bool()), R::rel()) -> rel()

Filter a temporal relation by a predicate on the range. filter(P, R) relates T to X, if R relates T to X and P(X) == true. P can be partial.

flatmap/2

flatmap(F::fun((term()) -> [term()]), R::rel()) -> rel()

Equivalent to elems(map(F, R)).

Apply a list valued partial function to the values of a temporal relation. map(F, R) relates T to Y if R relates T to X and F(X) contains Y. Values in the range of R for which F is not defined are discarded.

from_timed_list/1

from_timed_list(L::[{time(), term()}]) -> rel()

Construct a temporal relation from a list of time value pairs.

implies/2

implies(R1::rel(), R2::rel()) -> rel()

Equivalent to union(negation(R1), R2).

Relational implication. Relates T to none when the condition is not satisfied.

intersection/2

intersection(R1::rel(), R2::rel()) -> rel()

Intersection of two temporal relations. intersection(R1, R2) relates T to X, if both R1 and R2 relates T to X.

is_false/1

is_false(R::rel()) -> bool()

Check if a temporal relation is empty. is_false(R) is true if R is the empty temporal relation.

is_subrelation/2

is_subrelation(R1::rel(), R2::rel()) -> bool()

Equivalent to is_false(subtract(R1, R2)).

Check if a temporal relation is a subrelation of another temporal relation.

is_true/1

is_true(R::rel()) -> bool()

Check if a temporal relation is total. is_true(R) is true if R relates every time to a value.

last/1

last(R::rel()) -> rel()

Extend a temporal relation to include the most recently related value. last(R) relates T to X, if R relates T' to X for the last time T' =< T in the domain of R.

map/2

map(F::fun((term()) -> term()), R::rel()) -> rel()

Apply a (partial) function to the values of a temporal relation. map(F, R) relates T to Y if R relates T to X and F(X) == Y. Values in the range of R for which F is not defined are discarded.

negation/1

negation(R::rel()) -> rel()

Equivalent to negation(none, R).

The negation of a temporal relation.

negation/2

negation(None::term(), R::rel()) -> rel()

The negation of a temporal relation. negation(None, R) relates T to None, if there is no X such that R relates T to X.

partition/2

partition(P::fun((term()) -> bool()), R::rel()) -> {rel(), rel()}

Partition a temporal relation based on its range. Returns one temporal relation with all the values from R satifying P and one with the values not satisfying P.

product/2

product(R1::rel(), R2::rel()) -> rel()

The product of two temporal relations. product(R1, R2) relates T to {X, Y} if R1 relates T to X and R2 relates T to Y.

range/1

range(R::rel()) -> [term()]

The range of a temporal relation. Returns the ordered list of all X such that R relates T to X for some T.

restrict/2

restrict(R::rel(), When::rel()) -> rel()

Restrict a temporal relation to the domain of another temporal relation. restrict(R, When) relates T to X, if R relates T to X and When relates T to some Y.

ret/1

ret(X::term()) -> rel()

A singleton temporal relation. ret(X) just relates 0 to X. (It is the return operation for the temporal relation monad.)

set/1

set(R::rel()) -> rel()

Converting a temporal relation to a set valued temporal relation. set(R) relates T to at(T, R).

shift/2

shift(Time::time(), R::rel()) -> rel()

Shift a temporal relation by a given time. shift(Time, R) relates T to X, if R relates T - Time to X. Note that if Time < 0 the initial part of R will be discarded, since the domain of a temporal relation only includes non-negative times.

slice/3

slice(T0::time(), T1::time(), R::rel()) -> rel()

Restrict a temporal relation to a particular time slice. slice(T0, T1, R) is the restriction of R to the domain T0 =< T < T1.

split_at/2

split_at(P::fun((term()) -> bool()), R::rel()) -> {rel(), rel()}

Split a temporal relation into two temporal relations with disjoint domains. The domain of the input temporal relation is split at the earliest occurrence of a value matching the given predicate.

stateful/3

stateful(Start::fun((term()) -> [State]), Transform::fun((State, term()) -> [State]), R::rel()) -> rel()

State = term()

Apply a simple state machine to a temporal relation. The Start function maps values to sets of initial states, and Transform maps a state and a value to a (potentially empty) set of new states. A state S is started at time T, if R relates T to X and Start(X) contains S. Whenever Transform(S, Y) is defined for any Y in R, then S is replaced by all the states in Transform(S, Y). Both Start and Transform can be partial.

Generated by EDoc