overturetool
History counters and permission predicates in the debugger
The ability to set break points at permission and inspect history counters (see #360) should already be present in the code base.
We need to investigate if this is possible and, if not, then it's a bug and we need to fix it.
Confirmed. Breakpoints can be set for permission predicates but the interpreter does not stop at them.
If you force a deadlock (for example, by adding a conjunction with false), the debugger will stop at the permission predicate but it is still not possible no inspect the history counters. In fact, it's not possible to inspect any variables.
I'm marking this as a bug and closing the original task.
I think I disabled the check for binary operators so that debugging was "sane" in some very complex pre/postconditions. These tend to have a long list of "and" clauses for the different aspects being verified. With the break on the operator (as opposed to the operands) stepping through the expression caused some very confusing "leaping about" because of the way a series of "and" clauses form the evaluation tree. So if you change this, create a specification with a long list of "and" clauses in a pre/post and try stepping through it to find out which clause "fails".
I'll post an example, to give you some idea...
The following is an example postcondition (actually a function, called as a postcondition) showing what I mean about a long list of "and" clauses. Debugging these is difficult unless the "step" flow jumps from clause to clause in the "top to bottom" order you would expect:
postRtsLineItemAdd: ARTS`RTSLineItemAdd * ARTS`RTSLineItemAddResponse * SessionState * SessionState +> bool
postRtsLineItemAdd(request, response, new, old) ==
-- req and resp are the request and response, respectively
let req = request.arg0, resp = response.retval in
-- If we have sent a retry repeat of the last response, then nothing
-- has changed except the lastRequestId, which has the new retry count,
-- and the lastResponseId, which is has an incrememnted logicalID.
if old.lastRequestId <> nil
and req.header.messageId.logicalID = old.lastRequestId.logicalID
and old.lastResponse <> nil
then
new.basket = old.basket
and new.basketState = old.basketState
and new.basketId = old.basketId
and new.lastSuccessId = old.lastSuccessId
and new.lastResponseId.logicalID = old.lastResponseId.logicalID + 1 -- Updated
and new.lastRequestId = req.header.messageId -- Updated
and resp = updatedResponse(old.lastResponse, new.lastResponseId, new.lastRequestId)
and new.lastResponse = resp
else
-- It must be a valid response
resp.header.actionCode = <ADD> and resp.header.messageType = <RESPONSE>
-- If there is a sequence error, then lastRequestId is not changed, otherwise
-- the lastRequestId is updated to that in the request header
and (if getError(resp) = INVALID_SEQUENCE
then new.lastRequestId = old.lastRequestId
else new.lastRequestId = req.header.messageId)
-- The last response (for retry calls) is the new response, even if
-- it is an error response.
and new.lastResponse = resp
-- And the lastResponseId has been incremented
and new.lastResponseId.logicalID = old.lastResponseId.logicalID + 1
-- And the response's messageID will match the lastResponseId
and resp.header.messageId = new.lastResponseId
-- And the response request ID will be the same as the request's ID
and resp.header.response.requestId = req.header.messageId
-- The last successful response is set to this responseId (even business
-- errors are considered successful - only system errors fail).
and new.lastSuccessId = new.lastResponseId
-- and the response carries the previous lastSuccessId value
and resp.header.response.lastSuccessfulResponseID = old.lastSuccessId
-- if the response is any sort of error, the Horizon basket and basket state
-- will not have changed, and there will be no POSLogs returned
and if isErrorResponse(resp)
then
new.basket = old.basket
and new.basketState = old.basketState
and new.basketId = old.basketId
and resp.posLog = nil
-- And the error is one of the following
and getError(resp) in set {
INVALID_REQUEST,
INVALID_SEQUENCE,
INVALID_BASKET_ID }
-- otherwise this is a successful response and everything that follows can
-- assume this:
else
-- If this was populated basket, the basketId hasn't changed since it was
-- It is changed by the first add to a NO_BASKET - note that it is
-- not a strict sequence
(old.basketState = <POPULATED_BASKET> => new.basketId = old.basketId)
-- The response carries the (possibly new) basketId back to the Terminal
and resp.posLog.sessionSequenceNumber = new.basketId
-- The BU/Till/Operator values have been set, if needed. The BU/till remain
-- set for the HTTP session
and areSetBUTillOperator(req, new.bu, new.till, new.operator)
-- The successful basket state is "POPULATED"
and new.basketState = <POPULATED_BASKET>
-- The POSLog returned consists of one POSLogRetailTransaction entry for the item
-- added to the Horizon basket.
and len resp.posLog.retailTransaction = 1
and resp.posLog.retailTransaction = [basketItemToLog(new.basket(len new.basket))]
-- If there was no basket before the call, then the new basket will have one
-- item in it, otherwise the basket size will have increased by one.
and (if old.basket = nil
then len new.basket = 1
else len new.basket = len old.basket + 1)
-- In either case, the last item in the basket will correspond to
-- the token lookup of the scan data passed in the request. We take
-- the BID/TID from the last entry, since these are set by HBS.
and let last = new.basket(len new.basket) in
last = logToBasketItem(req.posLog.retailTransaction(1), last.bid, last.tid);