Encoding flow expressions in Promela

[vrozen]

MM requires floating point calculations in flow expressions. The result of evaluating these expressions is to round down to the nearest integer number. How can MM expressions be supported?

Promela only supports integer expressions natively, since its values are "abstractions". It does however support embedding C code. The following model does not show the correct value in guided simulation but it does produce a verifier that seems to work correctly.

active proctype mm()
{
  int a = 0;
  c_code
  {
    Pmm -> a = 0.6 * 2;
  };
  printf("the value of a = %d\n", a);
  assert(a == 0);
}

This only works when taking the following steps

• generate a verifier rozen$ spin -a experiment.pml
• compile the verifier gcc pan.c
• run the verifier ./a.out
• play back the spin trail using the verifier /a.out -P experiment.pml.trail

 1: proc  0 (mm) experiment.pml:7 (state 1) [    Pmm -> a = 0.6 * 2;
  ]
the value of a = 1
pan:1: assertion violated (a==0) (at depth 2)
spin: trail ends after 2 steps
  2:    proc 0 (mm)  experiment.pml:8 (state  2) (invalid end state)
        printf('the value of a = %d\n',a)

[vrozen]

ToPromela now supports two ways of generating expressions based on a debug flag

1. native promela expressions (debug = true)
2. embedded c fragments (debug = false)

[vrozen]

The design decision of rounding down flow expressions to the nearest integer still seems good. Edges are memoryless and don't accumulate resources, flow only transports whole number resources and pools only store integer values. However, using floats to implement flow expressions is bad because of rounding errors.

Paul already mentioned we need fixed point instead of floating point. We should probably use decimal encoding making the scaling factor a power of ten. Assuming designers require no more precision than percentages, a fixed factor of 1/100 seems like a good choice. e.g. 1.23 = 123/100.

Fixed point arithmetic might be fully implemented in Promela, although I observed we can also fully implement node behaviors in C because they are deterministic. The advantage would be sharing MM library code with the analysis. The disadvantage would be even worse meta-level debugging, by excluding the use of the Spin interpreter. User-level debugging of Micro-Machinations Traces (.mmt) would not be affected.