Formal Systems Specification in AtelierB - Lhs of binary operator should be a sequence (given type is POW(POW(INTEGERS * ORDERs)))

Question

I am trying to develop a B specification for a small stock management system and I am battling with the error:

Lhs of binary operator should be a sequence (given type is POW(POW(INTEGERS * ORDERs)))

This is my Abstract Machine:

MACHINE
    stock(ORDER, order_limit)
CONSTRAINTS
    order_limit: NAT1
SETS
    PART_COSTS;
    PARTS;
    ORDERS
    
CONSTANTS
    backlog_limit
PROPERTIES 
    backlog_limit: NAT1 & backlog_limit <= 20
VARIABLES
    limit,
    backlog,
    part_quantity
INVARIANT 
    backlog = iseq(ORDERS) & limit : NAT1 & card(backlog) <= limit & limit <= 20 &
    part_quantity : NAT1 & part_quantity >= 200
INITIALISATION
    limit := order_limit || backlog := iseq(ORDERS) || part_quantity := 0
OPERATIONS

     receiveorder(order) =
        PRE 
            order : ORDER & limit > card(backlog)
        THEN
            backlog := backlog <- order
        END
END

I don't understand why I am getting this error since backlog is literally a sequence ( I initialised it as a sequence of the set (ORDERS)?

Answer 1

The first occurrence (after its declaration) of the symbol backlog is in the following typing predicate: backlog = iseq(ORDERS). So backlog is the set of all injective sequences of ORDERS values. You probably wanted to have backlog: iseq(ORDERS), i.e., backlog is some injective sequence of ORDERS.

Of course, you need to change the initialization for backlog. You may initialize it with:

• an empty sequence: backlog := []
• or any sequence backlog :: iseq(ORDERS)
• or any expression of type iseq(ORDERS)

Finally, in operation receiveorder, the type for the input parameter order should be the type of the elements of the backlog sequence, that is ORDERS, and not ORDER (and you do not need machine parameters).