--
-- IncDec System
--
-- Let us consider a system that consists of two processes,
-- which are called Inc and Dec.
-- The processes share one integer variable, say x.
-- Process Inc repeatedly increments variable x.
-- Process Dec decrements variable x provided that another
-- variable, say flag, is true.
--
-- x is initially set to 0, and flag is initially set to false.
-- flag is set to true by process Inc if it increments x.
-- flag is set to false by process Dec if it decrements x.
--
-- We are going to make a formal model of the system.
-- Formal models used are OTS's (observational transition systems).
-- You may regard OTS's as usual transition systems, which consist of
-- a set of transition rules and a set of variables, which have
-- initial values. 
-- The variable constitute the state space.
--
-- The formal model of the system: 
--  - Two transition rules are used:
--    * 'inc' increments x and sets flag to true.
--    * 'dec' decrements x and sets flag to false if flag is true.
--  - Two variables (observable values) are used:
--    * 'x'    denotes variable x, initially 0
--    * 'flag' denotes variable flag, initially false
--
-- The following is a possible execution of the transition system:
--
--    +----+        +----+        +----+        +----+
--    |x: 0|        |x: 1|        |x: 2|        |x: 1|
--    +----+ -inc-> +----+ -inc-> +----+ -dec-> +----+ ......
--    |f: f|        |f: t|        |f: t|        |f: f|
--    +----+        +----+        +----+        +----+
--
-- where f: stands for flag:, t and f for true and false.
--
-- It seems that x is always greater than or equal to 0 in the system.
-- But can you explain why it is?
-- We can do by writing proofs or proof scores in CafeOBJ.
-- Before that, we describe the transition system in CafeOBJ.
--

--
-- Some theorems about inequalities on integers are needed.
-- So, they are provided in module INT+.
-- We should prove them. But, we skip it in this seminar.
--
mod! INT+ {
  pr(INT)
  var X : Int
  ceq X + 1 >= 0 = true if X >= 0 .
  ceq X + 1 >= 1 = true if X >= 0 .
  ceq X + -1 >= 0 = true if X >= 1 .
}

--
-- The transition system is described in module INCDEC.
--
-- Hidden sort 'System' denotes the state space.
-- Constant    'init'   denotes any initial state.
-- Operation   'x'      denotes variable x.
-- Operation   'falg'   denotes variable flag.
-- Operation   'inc'    denotes transition rule inc.
-- Operation   'dec'    denotes transition rule dec.
--
-- {strat: (0 1)} is the local strategy given to operation c-dec.
-- But don't care, just think it as a magic word for a while.
--
-- Given a state s, 
-- inc(s) denotes the successor state after executing the transition
-- rule corresponding to inc, and 
-- dec(s) denotes the succrssor state after executing the 
-- transition rule corresponding to dec.
-- We define inc and dec by describing how the values of x and
-- flag change after executing the corresponding transition rules.
--
mod* INCDEC {
  pr(INT+)
  *[System]* 
-- any initial state
  op init : -> System
-- observations
  bop x    : System -> Int
  bop flag : System -> Bool  
-- actions
  bop inc : System -> System
  bop dec : System -> System
-- CafeOBJ variables
  var S : System
-- for any initial state
  eq x(init)    = 0 .
  eq flag(init) = false .
-- inc
  eq x(inc(S))    = x(S) + 1 .
  eq flag(inc(S)) = true .
-- dec
  op c-dec : System -> Bool {strat: (0 1)}
  eq c-dec(S) = flag(S) .
  --
  ceq x(dec(S))    = x(S) - 1 if c-dec(S) .
  ceq flag(dec(S)) = false    if c-dec(S) .
  ceq dec(S)       = S        if not c-dec(S) .
}

eof

--
-- We can simulate some possible executions of the system.
--
open INCDEC
  ops s1 s2 : -> System .
  eq s1 = dec(inc(inc(init))) .
  eq s2 = inc(inc(dec(dec(dec(dec(s1)))))) .
  red x(s1) .
  red x(s2) .
close
--
-- Such simulationns may allow you to understand the system more,
-- and may help you find some errors in the specification if any.
--
-- To understand the system profoundly, you can verify that the
-- system really has the properties that we expect the system to
-- have.
--