The Constraints Library

/* @provengo summon constraints */

Using this library, QA analysts can declaratively limit or require occurrences of events or event sets.

For example, to forever block event E after event F occurred, use:

Constraints.after(E).block(F).forever();

The structure of the constraint statements is as follows: First, we may specify a trigger event. We then add what to block or limit, and then the end condition - until forever or until a certain event occurs.

You must specify an end condition for the constraint to become active.

A constraint can be canceled before it is placed if a specified event is selected. This is done using the .unless call. For example, if we want to block B after E happened, unless U happened before E, we can write the first line in the code below. We can combine unless with until, to cancel this block whenever U happens - either before or after E ^[1].

// If `E` happened before `U`, block `B` forever.
Constraints.unless(U).after(E).block(B).forever();

// After `E` happens, block `B`. If U happens at any point, cancel this block.
Constraints.unless(U).after(E).block(B).until(U);

The constraints are placed globally. So your script continues to run after a .forever() constraint is placed.

Blocking Constraints

These constraints prevent events from happening. The are also known as safety requirements.

// @provengo summon constraints (1)

const E, F, G; // events

// E cannot happen.
Constraints.block(E).forever();
// E cannot happen before F.
Constraints.block(E).until(F);

// After E happens, never allow F.
Constraints.after(E).block(F).forever();
// F cannot happen between E and G.
Constraints.after(E).block(F).until(G);

// E can only happen 5 times.
Constraints.limit(E, 5).forever();

// E can only happen 5 times until F occurs (then it can
// occur as many times at it wants).
Constraints.limit(E, 5).until(F);

// E can happen up to 5 times (including) between G and F.
Constraints.after(G).limit(E, 5).until(F);

// blocks F after E occurs. F is unblocked after G occurs.
// This constraint is lifted when Z occurs before E does.
Constraints.unless(Z).after(E).block(F).until(G);

1	Bring the Constraints library into scope

Future Constraints

These constraints require that certain events would happen. They do not request the events, just verify that they eventually happen. These are also known as liveness requirements.

An example use is modeling a requirement such as every process has to eventually end. This requirement does not detail how it ends or what causes it to do so, just that a process cannot go on forever.

// @provengo summon constraints (1)

const A,B,C; // events

// A must be selected at some point in the future.
Constraints.require(A).eventually();

// A must be selected at some point in the future, unless B is selected.
Constraints.require(A).until(B);

// If A happens, then B must happen eventually.
Constraints.after(A).require(B).eventually();

// If A happens, then as long as C did not happen, B must happen eventually.
Constraints.after(A).require(B).until(C);

Example of Using Future Constraints

Future constraints can be used to find problems in a business process. Consider a simple quote-sale process. A user may visit a site, and request a quote. Given the quote, the user may buy or decline the quote altogether. The quote request, if submitted, it processed internally. This process should always result in a quote being delivered, but it’s not trivial to show that a process will always indeed deliver the quote.

We can use the Constraint library to ensure that the process works, like so (the full file can be found here):

// @provengo summon constraints

/* event definitions go here */

// After a quote is requested, it must eventually be handled.
Constraints.after(requestQuote)
           .require(quoteHandled)
           .eventually();

// A quote can't be handled until it is delivered.
Constraints.block(quoteHandled)
           .until(quoteDelivered);

Next, we model the "user view" of the process:

// "Customer view": visit, request (or leave), decline or buy
bthread("main process", function(){
    // Visit the site
    request(visitSite);

    // if decide to leave, abort
    interrupt( leaveSite, function(){
        // request quote or leave
        request([requestQuote, leaveSite]);
        // buy or decline
        request([saleDone, quoteDeclined]);
    });
});

Now, we add a set of behaviors modeling the internal process for quote creation. They wait for a quote request and try to provide a quote for it (full source here). Spoiler: there’s a logic bug here.

bthread("process1", function(){
    waitFor( requestQuote );
    interrupt( quoteDelivered, function(){
        request( process );
        request( process );
        request( process );
    });
});
bthread("process2", function(){
    waitFor( process[0].or(process[1]) );
    sync({
        block: process,
        request: quoteDelivered
    });
});

We can now ask provengo to draw the process - states where the system is bound by a future condition are red:

Figure 1. Buggy process - not all quote requests are handled. The red path shows how a quote request can get ignored because of a problem in the process.

1. Note that U and E cannot happen together, as only a single event is selected at each synchronization point.