module simulation

-- 			TYPES

sig Op {}

sig State {}

-- 			TRACES

sig Trace {}

disj sig EmptyTrace extends Trace {}

disj sig NonEmptyTrace extends Trace {
  prefix : Trace,
  last : Op
}

-- All traces are either empty or non-empty.
fact { Trace in EmptyTrace + NonEmptyTrace }

-- No trace can be prefixed by itself. 
fact { all t : Trace | t !in t.^prefix }

-- 			FAILURES

sig Refusal { ops : set Op }

sig Failure {
  trace : Trace,
  refusals : set Refusal
}

--			PROCESSES

sig Process {
  failures : set Failure
}

-- 		HEALTHINESS CONDITIONS

fact {
  all process : Process {
    let traces = process.failures.trace {
      -- the empty trace is a possible trace
      EmptyTrace in traces
      -- trace set is prefix closed
      traces.prefix in traces
    }
    all failure : process.failures {
      -- must have some refusals
      some failure.refusals
      all refusal : failure.refusals {
        -- refusal set is subset closed for every failure
        all op : refusal.ops { 
          some refusal' : failure.refusals |
            refusal'.ops = refusal.ops - op
        }
        -- traces and refusals are consistent:
          -- either a given trace can be extended by a given operation
          -- or that operation may be refused after the given trace
        all op : Op {
          some failure' : process.failures |
            ( failure'.trace = failure.trace &&
              failure.refusals.ops + op in failure'.refusals.ops )
            ||
            ( failure'.trace.prefix = failure.trace &&
              failure'.trace.last = op )
        }
      }
    }
    -- there is at most one failure for any given trace
    -- (this constraint ensures correct canonicalisation of failures)
    all failure, failure' : process.failures {     
      failure.trace = failure'.trace  
        =>  failure.refusals = failure'.refusals
    }
  }
} 

--			CANONICALIZATION

fact { 
  all t, t' : Trace {
    t.prefix = t'.prefix && t.last = t'.last  =>  t = t'
  }
  all r, r' : Refusal {
    r.ops = r'.ops  =>  r = r'
  }
  all f, f' : Failure {
    f.trace = f'.trace && f.refusals = f'.refusals  =>  f = f'
  }
  all p, p' : Process {
    p.failures = p'.failures  =>  p = p'
  }
  all d, d' : DataType {
    (d.state = d'.state && d.init = d'.init && d.names = d'.names 
     && d.trans = d'.trans)  =>  d = d'
  }
  all m, m' : Machine { 
    (m.datatype = m'.datatype && m.after = m'.after && 
     m.process = m'.process)  =>  m = m'
  }
  all p, p' : Pair {
    (p.abstract = p'.abstract && p.concrete = p'.concrete)  
    =>  p = p'
  }    
}

-- 			ABSTRACT DATA TYPES

-- We give a generic definifition so we may reason later about data
-- types with the same state space and data types with different state
-- spaces.

sig DataType {
  state : set State,
  init : set state,
  names : set Op,
  trans : names ->+ state -> state
} {
  some init && some names
}

-- 			CORRESPONDING PROCESSES

-- A "machine" associates data types and their corresponding
-- processes, employing a function after which relates traces with
-- states that could be reached after the given trace.

sig Machine {
  datatype : DataType,
  after : Trace -> State,
  process : Process
} {
  -- only give after states for possible traces of the process
  after.State = process.failures.trace
  -- traces may include only operations defined on the data type
  process.failures.trace.last in datatype.names
}

--  Recalling that a process is defined by its semantic model:
--  Each semantic model relates the variables "datatype", "after" and
--  "process" of machines.


--			SEMANTICS

-- Linking traces and after states.
fact { 
  all m : Machine {
    let traces = m.process.failures.trace {
      -- base case
      m.after[EmptyTrace] = m.datatype.init
      -- inductive step
      all trace : traces - EmptyTrace {
        m.after[trace] = 
          m.after[trace.prefix].(m.datatype.trans[trace.last])
      }
    } 
    -- an operation can be performed after a given trace precisely
    -- when there is an after state of the trace that lies in the
    -- domain of the operation.
    all failure : m.process.failures, op : m.datatype.names {
      (some (m.datatype.trans[op]).State & m.after[failure.trace]) <=>
        (some failure' : m.process.failures | 
           failure'.trace.prefix = failure.trace && 
           failure'.trace.last = op)    
    }
  }
}

-- Linking failures and after states.
fact {
  all m : Machine {
    -- a set of operations can be refused after a given trace precisely
    -- when there is an after state of the trace that lies outside the
    -- domains of all the operation.    
    all failure : m.process.failures, op : m.datatype.names {
      all ref : failure.refusals {
        (some ref' : failure.refusals | ref'.ops = ref.ops + op) <=>
          (some m.after[failure.trace] 
             - (m.datatype.trans[ref.ops + op]).State)
      }
    }
  }
}
     
--			PROCESS REFINEMENT

fun StableFailuresRefinedBy (a,c : Process) {
  all failure : c.failures {
    -- if a set of events can be refused after a given trace in the
    -- concrete model then it must have been possible in the abstract
    -- model to refuse the given set of events after the given trace.
    all ref : failure.refusals {
      some failure' : a.failures |
        failure'.trace = failure.trace && ref in failure'.refusals
    }
  } 

}

fun SingletonFailuresRefinedBy (a,c : Process) {
  all failure : c.failures {
    -- if a set of events of cardinality at most one can be refused
    -- after a given trace in the concrete model then it must have
    -- been possible in the abstract model to refuse the given set of
    -- events after the given trace.
    all ref : failure.refusals {
      (! sole ref.ops ) 
      ||
      ( some failure' : a.failures |
          failure'.trace = failure.trace && ref in failure'.refusals)
    }
  } 
}
  
--			SIMULATION

-- There are many different sets of simulation rules for data types:

-- For now we consider simulation rules fordata refinement of systems
-- with an implicit notion of communication and we adopt a blocking
-- interpretation.  Moreover, since the rules corresponding to data
-- types with the same state space are simply a special case of the
-- rules corresponding to data types with different state spaces, we
-- will assume that their state spaces are different.

sig Pair {
  -- A pair comprises an abstract and a concrete Machine and a
  -- retrieve relation relating their state spaces.
  abstract : Machine,
  concrete : Machine,
  retr : State -> State
} 

fun SimulatesFwds (pair : Pair) {

  let A = pair.abstract.datatype,
      C = pair.concrete.datatype,
      AState = pair.abstract.datatype.state,
      CState = pair.concrete.datatype.state,
      R = pair.retr {

      -- Forwards retrieve relation
      R.State in AState && State.R in CState    

      -- The models share the same operations.  
      A.names = C.names

      -- The concrete initialisation is consistent with the abstract
      -- initialisation.
      C.init in (A.init).R
  
      -- All concrete operations are consistent with their corresponding
      -- abstract operations.
      all n : A.names | R.(C.trans[n]) in (A.trans[n]).R

      -- Each concrete operation is available precisely when the
      -- corresponding abstract operation is available.
      all n : A.names |  
        ((A.trans[n]).AState).R in (C.trans[n]).CState
  }
}

fun SimulatesBkwds (pair : Pair) {

  let A = pair.abstract.datatype,
      C = pair.concrete.datatype,
      AState = pair.abstract.datatype.state,
      CState = pair.concrete.datatype.state,
      R = pair.retr {

      -- Backwards retrieve relation
      R.State in CState && State.R in AState    

      -- The models share the same operations.  
      A.names = C.names

      -- The concrete initialisation is consistent with the abstract
      -- initialisation.
      (C.init).R in A.init
  
      -- All concrete operations are consistent with their corresponding
      -- abstract operations.
      all n : A.names | (C.trans[n]).R in R.(A.trans[n])

      -- Each concrete operation is available precisely when the
      -- corresponding abstract operation is available.
      all n : A.names |
        (CState - (C.trans[n]).CState) in 
           R.(AState - (A.trans[n]).AState)

      -- Applicability of retrieve relation.
      CState in R.AState
  }
}

-- 		VERIFYING SOUNDNESS OF SIMULATION RULES
 
assert FwdsSimulationSoundForSingletonFailures {
  all pair : Pair {
    SimulatesFwds (pair) => 
      SingletonFailuresRefinedBy (pair.abstract.process, 
                                  pair.concrete.process)
  }
}

assert BkwdsSimulationSoundForSingletonFailures {
  all pair : Pair {
    SimulatesBkwds (pair) => 
      SingletonFailuresRefinedBy (pair.abstract.process, 
                                  pair.concrete.process)
  }
}

assert FwdsSimulationSoundForStableFailures {
  all pair : Pair {
    SimulatesFwds (pair) => 
      StableFailuresRefinedBy (pair.abstract.process, 
                               pair.concrete.process)
  }
}

assert BkwdsSimulationSoundForStableFailures {
  all pair : Pair {
    SimulatesBkwds (pair) => 
      StableFailuresRefinedBy (pair.abstract.process, 
                               pair.concrete.process)
  }
}

check FwdsSimulationSoundForSingletonFailures for 3 but 1 Pair
check BkwdsSimulationSoundForSingletonFailures for 3 but 1 Pair

check FwdsSimulationSoundForStableFailures   
  for 2 but 1 Pair, 4 Failure, 4 Refusal, 4 State, 3 Trace

check BkwdsSimulationSoundForStableFailures   
  for 2 but 1 Pair, 4 Failure, 4 Refusal, 4 State, 3 Trace