Contract file

The contract file contains a string representation of the contract to monitor. The formula is expressed in a logic called LTL-FO+. You don't need to express your contract directly into LTL-FO+; there exists tools that converts easier notations, such as UML Sequence Diagrams, into LTL-FO+.

Learn more about specifying contracts.

# ---------------------------------------------------------------
# BeepBeep contract file for the simple library example
# For more info:
# ---------------------------------------------------------------
% All "return" messages must precede any "borrow" message
; G ([x1 /message/action] (((x1) = ({borrow})) -> 
  (X (G ([x2 /message/action] (!((x2) = ({return}))))))))
% The time elapsed between the first and second message must be less than 5 secs
; [x1 $_TIME] (X ([x2 $_TIME] (((x2) - (x1)) < ({5}))))
% A book that is borrowed cannot be borrowed again until is has been returned
; G ([x1 /message/action] (((x1) = ({borrow})) ->
  ([x2 /message/books/book] (X ((!(<x3 /message/action>
    (((x3) = ({borrow})) & (<x4 /message/books/book> ((x2) = (x4))))))
      U (<x5 /message/action> (((x5) = ({return})) &
        (<x6 /message/books/book> ((x2) = (x6))))))))))

Main menu Logo