PTA, Digital Clocks, Negation

[proteusGIT]

I understand that strict clock comparisons of the form x<2 are prohibited for the digital clocks engine. But apparently, negation is not and, hence, x<2 can be encoded using !(x>=2). Then I also recognized that PRISM rewrote the condition Pmax=? [ F !(x>=2) ] into Pmax=? [ F !(x*2>=2) ]. While x*2 may be an internal name for a fresh variable, I was wondering if there may be a bug here.

Basically, I just wanted to get a full grammar of what PRISM supports for each of the three PTA engines.

Model checking: Pmax=? [ F !(x>=2) ]

Performing digital clocks translation...
Computed clock maximums: {x=2, y=10}
Computed GCD: 2

Type:        MDP
Modules:     M 
Variables:   s x y 

Model checking: Pmax=? [ F !(x*2>=2) ]

Building model...

model:

pta

module M

    s : [0..3] init 0;
    x : clock;
    y : clock;

    []
        s=0
        -> 
        0.5: (s'=1)&(x'=0)
        +
        0.5: (s'=2);
    []
        s=1 & x=0 & y=10
        -> 
        1: (s'=3) & (y'=0);
    []
        s=2 & x=0 & y=0
        -> 
        1: (s'=3);

endmodule

label "success" = (s=3);

[davexparker]

The example above (!(x>=2)) is a case of PRISM not being rigorous enough in its enforcement of the digital clocks engine restrictions. This should be disallowed really. Which is not to say that there is a definitely a problem with this particular example, but this trick would allow problematic models to slip through.

The conversion of x to x*2 is a PRISM optimisation. Note the line Computed GCD: 2 in the output. We compute the greatest common denominator of the constants compared to clocks (0, 2, 10 in this case) and re-scale the model accordingly for efficiency.

The summary of restrictions for each engine is given on this page of the manual:

http://www.prismmodelchecker.org/manual/PropertySpecification/PTAProperties

See also this tutorial paper for more in-depth discussion:

http://www.prismmodelchecker.org/bibitem.php?key=NPS13

[proteusGIT]

Ok thanks! It seems that similar checks are also not performed for the guards of PTA edges.