THEORY
  IMPORT THEORY PROJECTS
    /SimpleDEq THEORIES /SimpleDEq/LinComb.dtf|org.eventb.theory.core.deployedTheoryRoot#LinComb
  DATA TYPES
    Status
    CONSTRUCTORS
      ValveOpen()
      ValveClosed()
    InOutValve
    CONSTRUCTORS
      InOut(in_status:Status,out_status:Status)
  OPERATORS
    openIn expression (iov: InOutValve)
    closeIn expression (iov: InOutValve)
    openOut expression (iov: InOutValve)
    closeOut expression (iov: InOutValve)
    rstatus expression (st: Status)
    in_rstatus expression (iov: InOutValve)
    out_rstatus expression (iov: InOutValve)
    InOutPossible expression ()
      direct definition 
        { InOut(ValveOpen,ValveOpen),
          InOut(ValveOpen,ValveClosed),
          InOut(ValveClosed,ValveOpen),
          InOut(ValveClosed,ValveClosed) }
END