Assumptions

[lou1306]

Sometimes, full non-deterministic initialization can include more states than the ones the user is interested in verifying.

For instance, suppose the user wants to check that two robots never occupy the same position in a 10x10 grid. She defines the robots as follows:

agent Robot {
    interface = x: 0..10, y: 0..10
    # ...
}

But then, the property trivially fails because there are initial states where the robots start in the same position.

Proposal

Introduce a new section

assume {
    A1 = initially φ
    A2 = always φ
}

where φ follows the syntax of LAbS properties.

• initially assumptions are placed at the end of the init function;
• always assumptions are enforced at the head of the scheduler loop.

[lou1306]

Partially implemented in bc4e25a0b302b5f8d34f82bc932b5b4f52400b7c

• The assume { ... } block only allows specifying constraints on the initial state (initially φ in the original proposal)
• Modalities have been removed (assumptions are in the form Name = predicate)