Theory SLin

(* Author: Giuliano Losa *)

section ‹The SLin Automata specification›

theory SLin
imports IOA RDR
begin

datatype ('a,'b,'c,'d)SLin_action =
― ‹The nat component is the instance number›
  Invoke nat 'b 'c
| Response nat 'b 'd
| Switch nat 'b 'c 'a
| Recover nat
| Linearize nat

datatype SLin_status = Sleep | Pending | Ready | Aborted

record ('a,'b,'c)SLin_state = 
  pending :: "'b ⇒ 'b × 'c"
  initVals :: "'a set"
  abortVals :: "'a set"
  status :: "'b ⇒ SLin_status"
  dstate :: 'a
  initialized :: bool

locale SLin = RDR + IOA
begin

definition
  asig :: "nat ⇒ nat ⇒ ('a,'b,'c,'d)SLin_action signature" 
  ― ‹The first instance has number 0›
  where
  "asig i j ≡ ⦇
    inputs = {act . ∃ p c iv i' .
      (i ≤ i' ∧ i' < j ∧ act = Invoke i' p c) ∨ (i > 0 ∧ act = Switch i p c iv)},
    outputs = {act . ∃ p c av i' outp . 
      (i ≤ i' ∧ i' < j ∧ act = Response i' p outp) ∨ act = Switch j p c av},
    internals = {act. ∃ i' . i ≤ i' ∧ i' < j 
      ∧ (act = Linearize i' ∨ act = Recover i')} ⦈"

definition pendingReqs :: "('a,'b,'c)SLin_state ⇒ ('b×'c) set"
  where
  "pendingReqs s ≡ {r . ∃ p . 
     r = pending s p
     ∧ status s p ∈ {Pending, Aborted}}"

definition Inv :: "'b ⇒ 'c 
  ⇒ ('a,'b,'c)SLin_state ⇒ ('a,'b,'c)SLin_state ⇒ bool"
where
  "Inv p c s s' ≡ 
    status s p = Ready
    ∧ s' = s⦇pending := (pending s)(p := (p,c)),
        status := (status s)(p := Pending)⦈"

definition pendingSeqs where
  "pendingSeqs s ≡ {rs . set rs ⊆ pendingReqs s}"
  
definition Lin :: "('a,'b,'c)SLin_state ⇒ ('a,'b,'c)SLin_state ⇒ bool" 
where
  "Lin s s' ≡ ∃ rs ∈ pendingSeqs s .
      initialized s 
      ∧ (∀ av ∈ abortVals s . (dstate s) ⋆ rs ≼ av) 
      ∧ s' = s⦇dstate := (dstate s) ⋆ rs⦈"

definition initSets where
  "initSets s ≡ {ivs . ivs ≠ {} ∧ ivs ⊆ initVals s}"

definition safeInits where
  "safeInits s ≡ if initVals s = {} then {}
    else {d . ∃ ivs ∈ initSets s . ∃ rs ∈ pendingSeqs s .
      d = ⨅ivs ⋆ rs ∧ (∀ av ∈ abortVals s . d ≼ av)}"
      
definition initAborts where
  "initAborts s ≡ { d .dstate s ≼ d
    ∧ ((∃ rs ∈ pendingSeqs s . d = dstate s ⋆ rs)
      ∨ (∃ ivs ∈ initSets s . dstate s ≼ ⨅ivs 
        ∧ (∃ rs ∈ pendingSeqs s . d = ⨅ivs ⋆ rs))) }"
definition uninitAborts where
  "uninitAborts s ≡ { d .
    ∃ ivs ∈ initSets s . ∃ rs ∈ pendingSeqs s . 
      d = ⨅ivs ⋆ rs }"

definition safeAborts::"('a,'b,'c)SLin_state ⇒ 'a set" where
  "safeAborts s ≡ if initialized s then initAborts s
    else uninitAborts s"
  
definition Reco :: "('a,'b,'c)SLin_state ⇒ ('a,'b,'c)SLin_state ⇒ bool"
where
  "Reco s s' ≡  
      (∃ p . status s p ≠ Sleep)
      ∧ ¬ initialized s
      ∧ (∃ d ∈ safeInits s . 
        s' = s⦇dstate := d, initialized := True⦈)"
      
definition Resp :: "'b ⇒ 'd ⇒ ('a,'b,'c)SLin_state ⇒ ('a,'b,'c)SLin_state ⇒ bool"
where
  "Resp p ou s s' ≡  
      status s p = Pending 
      ∧ initialized s
      ∧ contains (dstate s) (pending s p)
      ∧ ou = γ (dstate s) (pending s p)
      ∧ s' = s ⦇status := (status s)(p := Ready)⦈"

definition Init :: "'b ⇒ 'c ⇒ 'a 
  ⇒ ('a,'b,'c)SLin_state ⇒ ('a,'b,'c)SLin_state ⇒ bool"
where
  "Init p c iv s s' ≡
    status s p = Sleep
    ∧ s' = s ⦇initVals := {iv} ∪ (initVals s), 
        status := (status s)(p := Pending), 
        pending := (pending s)(p := (p,c))⦈"
      
definition Abort :: "'b ⇒ 'c ⇒ 'a 
  ⇒ ('a,'b,'c)SLin_state ⇒ ('a,'b,'c)SLin_state ⇒ bool"
where
  "Abort p c av s s' ≡
     status s p = Pending ∧ pending s p = (p,c)
     ∧ av ∈ safeAborts s
     ∧ s' = s⦇status := (status s)(p := Aborted), 
      abortVals := (abortVals s ∪ {av})⦈"

definition trans where
"trans i j ≡ { (s,a,s') . case a of 
  Invoke i' p c ⇒ i ≤ i' ∧ i < j ∧ Inv p c s s'
| Response i' p ou ⇒ i ≤ i' ∧ i < j ∧ Resp p ou s s'
| Switch i' p c v ⇒ (i > 0 ∧ i' = i ∧ Init p c v s s') 
    ∨ (i' = j ∧ Abort p c v s s')
| Linearize i' ⇒ i' = i ∧ Lin s s'
| Recover i' ⇒ i > 0 ∧ i' = i ∧ Reco s s' }"

definition start where
  "start i ≡ { s . 
    ∀ p . status s p = (if i > 0 then Sleep else Ready) 
    ∧ dstate s = ⊥
    ∧ (if i > 0 then ¬ initialized s else initialized s)
    ∧ initVals s = {}
    ∧ abortVals s = {}}"

definition ioa where
  "ioa i j ≡
     ⦇ioa.asig = asig i j ,
      start = start i,
      trans = trans i j⦈"

end

end