Overview

• Description
• Data Types
• Function Index
• Function Details

Copyright © Quviq AB, 2008-2017

Version: 1.42.1

Description

Timed Traces of Events

 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}}].
 

Building a Temporal Relation

 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

 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}]}]
 

• 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.

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

Tracking Messages in Flight

 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,[]}]
 

Checking Deadlines

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

Making a Property

 Overdue == eqc_temporal:empty()
 

 eqc_temporal:is_false(Overdue)
 

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).
 

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

Tolerating Uncertainty

 CertainlyLoggedIn = all_past(4,LoggedIn)
 

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

Function Details

all_future/1

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

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

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

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

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

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

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

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

Compute the values related to Time by R.

bind/2

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 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

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

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

Turn a temporal relation into a total temporal relation.

constant/1

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

domain_size/1

The total time during which a temporal relation is true.

elems/1

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

The empty temporal relation.

filter/2

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

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

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

implies/2

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

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

intersection/2

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

is_false/1

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

is_subrelation/2

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

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

is_true/1

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

last/1

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

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

Equivalent to negation(none, R).

The negation of a temporal relation.

negation/2

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 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

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

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 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

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

set/1

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

shift/2

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

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 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

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.

subtract/2

Subtract one temporal relation from another. subtract(R1, R2) relates T to X, if R1 relates T to X and R2 does not relate T to X.

union/2

Union of two temporal relations. union(R1, R2) relates T to X, if one or both of R1 and R2 relates T to X.

unions/1

Take the union of a list of temporal relations.

Overview