Implicit operations does not take the frame condition into account in debugger

[pglvdm]

For a CML model such as:

     types
        Value = nat
        CellId = nat inv id == id > 0 and id <= maxring
        Direction =  <req> | <ack>

    values
        maxbuff = 4
        maxring = maxbuff - 1

    channels
        input, output : Value
        write, read: CellId * Direction * Value
        rrd, wrt: Direction * Value
        rd_i, wrt_i: CellId * Direction * Value

    process RingCell =
    begin
        state v:Value

        operations
            setV:Value ==> ()
            setV(x) ==
               v := x

            OrigsetV(x:Value)
                frame wr v
                post v = x

        actions
            Act = wrt.<req>?x -> wrt.<ack>.x -> setV(x); Act
                  []
                  rrd.<req>?dumb -> rrd.<ack>!v -> Act

        @ Act
    end

    process Controller =
    begin
        state cache:Value
              size:nat
              top:CellId
              bot:CellId

        operations
            Init: Value * nat * CellId * CellId ==> ()
            Init(c,s,t,b) ==
              (cache := c;
               size := s;
               top := t;
               bot := b)

             ExplSetCache: Value ==> ()
             ExplSetCache(x) ==
                cache := x

            ExplSetSize: nat ==> ()
            ExplSetSize(x) ==
               size := x

            ExplSetTop: CellId ==> ()
            ExplSetTop(x) ==
              top := x

            ExplSetBot: CellId ==> ()
            ExplSetBot(x) ==
              bot := x

             InitOrig(c:Value, s:nat, t:CellId, b:CellId)
                post cache=c and size=s and top=t and bot=b

            SetCache(x:Value)
                frame wr cache:Value
                post cache = x

            SetSize(x:nat)
                frame wr size:nat
                post size = x

            SetTop(x:CellId)
                frame wr top:CellId
                post top = x

            SetBot(x:CellId)
                frame wr bot:CellId
                post bot = x

        actions
            Input =
                [size < maxbuff] &
                    input?x ->
                        ( [size = 0] & SetCache(x); SetSize(1)
                          []
                          [size > 0] &
                                write.top.<req>!x -> write.top.<ack>?dumb ->
                                SetSize(size+1);
                                SetTop((top mod maxring)+1) )

            Output =
                [size > 0] &
                    output!cache ->
                        ( [size > 1] &
                            (|~| dumb:Value @
                                read.bot.<req>.dumb -> read.bot.<ack>?x -> Skip);
                            SetSize(size-1);
                            SetBot((bot mod maxring)+1)
                          []
                          [size = 1] &
                            SetSize(0))

        @ Init(0,0,1,1); mu X @ ((Input [] Output); X)
    end

one can debug and already after the first step:

[input.1]

It is clear that the ProB instantiation of the interpretation of implicit operations does not take the framing condition into account. The log-file shows this with:

Solver input:
            cache~:NAT & 
            cache:NAT & 
            (size~:NAT & 
            size:NAT) & 
            (top~:NAT & 
            top:NAT) & 
            (bot~:NAT & 
            bot:NAT) & 
            (cache~=0 & 
            bot~=1 & 
            top~=1 & 
            size~=0 & 
            cache=x) & 
            x=1
Solver solution:
            cache = 1
            bot = 0
            top = 0
            size = 0

where top before was 1 it is now set to 0 in the solution. This means that the constraint that all state components that are not mentioned in the ext clause are unchanged are not respected. So in this case one should use an additional conjunct like:

cache = cache~and top = top~and bot = bot~

[lausdahl]

I didn't check this model, but the current translation only considers explicit frame conditions. This means that rd must be present else it will be considers as wr, which is the opposite as VDM (is because it isn't implemented).

[pglvdm]

This is clearly wrong since "rd" should only be included in case one actually reads a particular state component. Anything not mentioned at all should definitely not be allowed to be changed in any notation.

[lausdahl]

See previous message. It is just not implemented.

[lausdahl]

Proper handling of frames have been added in overture

sync required

overturetool/overture@ac79e306436b68804b232f03755aca006dd34fa8