Using wait-for and blocking for refining models

Exercise: Refining the the interleavings of two stories

Open your terminal and navigate to a directory where you have write permissions. Execute the following command and respond to the prompts:

$ provengo create refining-the-model

This will generate a directory named refining-the-model, which contains a hello_world.js file located in the spec/js subdirectory. Clear the content of this file (you can also rename it) and replace with:

bthread("Adding product A, B, and C", function () {
    sync({ request: Event('AddProductToCart', { name: 'A' }) })
    sync({ request: Event('AddProductToCart', { name: 'B' }) })
    sync({ request: Event('AddProductToCart', { name: 'C' }) })
})

bthread("Adding product 1, 2, and 3", function () {
    sync({ request: Event('AddProductToCart', { name: '1' }) })
    sync({ request: Event('AddProductToCart', { name: '2' }) })
    sync({ request: Event('AddProductToCart', { name: '3' }) })
})

Now, if you run

$ provengo analyze --style full -f pdf refining-the-model

you should get the file refining-the-model/products/run-source/testSpace.pdf that looks similar to:

Test Space Before Your Code

Your task is to implement code that enforces the following sequence of events:

  • The action AddProductToCart {name:"A"} must be executed before AddProductToCart {name:"1"}.

  • The action AddProductToCart {name:"B"} must be executed before AddProductToCart {name:"2"}.

  • The action AddProductToCart {name:"C"} must be executed before AddProductToCart {name:"3"}.

Upon successful implementation, your code should shape the state space as follows:

Test Space With Your Code

If you get a different result, try to figure out what went wrong. If you get stuck, you can find the solution in the refining-the-model/solution directory.