Differences Between Regular JavaScript and Provengo JavaScript

While Provengo’s JavaScript variant is very similar to mainstream JavaScript, some differences exist. Some of these issues are due to the fact that when working with Provengo, you create models rather than programs. This drives a lot of changes in the threading models, data comparison approach, etc.

  • BThreads should never exchange data directly or though common data structures. They can only exchange data using events or bp.store.

    • This means no changing global variables. It is perfectly OK to read them, but don’t update them.

      • Use bp.store if you need a common place to store mutable data.

  • let vs const:

    • In the global program scope, prefer const.

    • In bthread bodies (and more generally, in code that can run within bthreads), always use let.

  • When comparing events (e.g. for a bthread deciding how to advance, when creating a script/manual test, or when evaluating an ensemble), prefer the use of contains to equals and ==. So e1.contains(e2) is better and more robust than e1==e2 or e1.equals(e2).

  • When comparing strings, prefer the == operator to ===.

  • Using sync points as arguments to methods/boolean condition (e.g. anArray.push( waitFor(es) ) might not work well with analyze.

Tips for Smaller Scenario Space

Some natural chioces for programmatic Javascript can cause state-space inflation when writing code for analysis. The generated scenarios are not wrong (that is, the sequence of events still makes sense) but visualizations and verifications might be more verbose that they could be. Here is how to keep the scenario space small:

Variable Usage

Do not use let in loops. Instead, define the variable above the loop and set it to undefined. Then, set it to undefined at the end of the loop’s body.

// bad:
while (true) {
    let e = waitFor(any(/shmoop/));
    request(Event(e.data.moop));
}

// good:
let e = undefined;
while (true) {
    e = waitFor(any(/shmoop/));
    request(Event(e.data.moop));
    e = undefined;
}

Don’t Mix sync and return

Do not use sync or its aliases (request, waitFor, etc.) in a return statement. Instead, store the value to be returned in a temporary variable, and then return it.

// bad:
function getDataOf(evtName) {
    return waitFor(any(evtName)).data;
}

// good:
function getDataOf(evtName) {
    let retVal = waitFor(any(evtName)).data;
    return retVal;
}
Some (hopefully all) of these differences will be solved in future versions of the tool.