Theory Promela
section "Formalization of Promela semantics"
theory Promela
imports
PromelaDatastructures
PromelaInvariants
PromelaStatistics
begin
text ‹Auxiliary›
lemma mod_integer_le:
‹x mod (a + 1) ≤ b› if ‹a ≤ b› ‹0 < a› for a b x :: integer
using that including integer.lifting proof transfer
fix a b x :: int
assume ‹0 < a› ‹a ≤ b›
have ‹x mod (a + 1) < a + 1›
by (rule pos_mod_bound) (use ‹0 < a› in simp)
with ‹a ≤ b› show ‹x mod (a + 1) ≤ b›
by simp
qed
lemma mod_integer_ge:
‹b ≤ x mod (a + 1)› if ‹b ≤ 0› ‹0 < a› for a b x :: integer
using that including integer.lifting proof transfer
fix a b x :: int
assume ‹b ≤ 0› ‹0 < a›
then have ‹0 ≤ x mod (a + 1)›
by simp
with ‹b ≤ 0› show ‹b ≤ x mod (a + 1)›
by simp
qed
text ‹
After having defined the datastructures, we present in this theory how to construct the transition system and how to generate the successors of a state, \ie the real semantics of a Promela program.
For the first task, we take the enriched AST as input, the second one operates on the transition system.
›
subsection ‹Misc Helpers›
definition add_label :: "String.literal ⇒ labels ⇒ nat ⇒ labels" where
"add_label l lbls pos = (
case lm.lookup l lbls of
None ⇒ lm.update l pos lbls
| Some _ ⇒ abortv STR ''Label given twice: '' l (λ_. lbls))"
definition min_prio :: "edge list ⇒ integer ⇒ integer" where
"min_prio es start = Min ((prio ` set es) ∪ {start})"
lemma min_prio_code [code]:
"min_prio es start = fold (λe pri. if prio e < pri then prio e else pri) es start"
proof -
from Min.set_eq_fold have "Min (set (start # map prio es)) = fold min (map prio es) start" by metis
also have "... = fold (min ∘ prio) es start" by (simp add: fold_map)
also have "... = fold (λe pri. if prio e < pri then prio e else pri) es start" by (auto intro!: fold_cong)
finally show ?thesis by (simp add: min_prio_def)
qed
definition for_all :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"for_all f xs ⟷ (∀x ∈ set xs. f x)"
lemma for_all_code[code]:
"for_all f xs ⟷ foldli xs id (λkv σ. f kv) True"
by (simp add: for_all_def foldli_conj)
definition find_remove :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a option × 'a list" where
"find_remove P xs = (case List.find P xs of None ⇒ (None, xs)
| Some x ⇒ (Some x, List.remove1 x xs))"
lemma find_remove_code [code]:
"find_remove P [] = (None, [])"
"find_remove P (x#xs) = (if P x then (Some x, xs)
else apsnd (Cons x) (find_remove P xs))"
by (induct xs) (auto simp add: find_remove_def dest: find_SomeD split: option.split)
lemma find_remove_subset:
"find_remove P xs = (res, xs') ⟹ set xs' ⊆ set xs"
unfolding find_remove_def
using set_remove1_subset
by (force split: option.splits)
lemma find_remove_length:
"find_remove P xs = (res, xs') ⟹ length xs' ≤ length xs"
unfolding find_remove_def
by (induct xs arbitrary: res xs') (auto split: if_splits option.splits)
subsection ‹Variable handling›
text ‹
Handling variables, with their different scopes (global vs. local),
and their different types (array vs channel vs bounded) is one of the main challenges
of the implementation.
›
fun lookupVar :: "variable ⇒ integer option ⇒ integer" where
"lookupVar (Var _ val) None = val"
| "lookupVar (Var _ _) (Some _) = abort STR ''Array used on var'' (λ_.0)"
| "lookupVar (VArray _ _ vals) None = vals !! 0"
| "lookupVar (VArray _ siz vals) (Some idx) = vals !! nat_of_integer idx"
primrec checkVarValue :: "varType ⇒ integer ⇒ integer" where
"checkVarValue (VTBounded lRange hRange) val = (
if val ≤ hRange ∧ val ≥ lRange then val
else
if lRange = 0 ∧ val > 0
then val mod (hRange + 1)
else
abort STR ''Value overflow'' (λ_. lRange))"
| "checkVarValue VTChan val = (
if val < min_var_value ∨ val > max_var_value
then abort STR ''Value overflow'' (λ_. 0)
else val)"
lemma [simp]:
"variable_inv (Var VTChan 0)"
by simp
context
fixes type :: varType
assumes "varType_inv type"
begin
lemma checkVarValue_bounded:
"checkVarValue type val ∈ {min_var_value..max_var_value}"
using ‹varType_inv type›
by (cases type) (auto intro: mod_integer_le mod_integer_ge)
lemma checkVarValue_bounds:
"min_var_value ≤ checkVarValue type val"
"checkVarValue type val ≤ max_var_value"
using checkVarValue_bounded [of val] by simp_all
lemma checkVarValue_Var:
"variable_inv (Var type (checkVarValue type val))"
using ‹varType_inv type› by (simp add: checkVarValue_bounds)
end
fun editVar :: "variable ⇒ integer option ⇒ integer ⇒ variable" where
"editVar (Var type _ ) None val = Var type (checkVarValue type val)"
| "editVar (Var _ _) (Some _) _ = abort STR ''Array used on var'' (λ_. Var VTChan 0)"
| "editVar (VArray type siz vals) None val = (
let lv = IArray.list_of vals in
let v' = lv[0:=checkVarValue type val] in
VArray type siz (IArray v'))"
| "editVar (VArray type siz vals) (Some idx) val = (
let lv = IArray.list_of vals in
let v' = lv[(nat_of_integer idx):=checkVarValue type val] in
VArray type siz (IArray v'))"
lemma editVar_variable_inv:
assumes "variable_inv v"
shows "variable_inv (editVar v idx val)"
proof (cases v)
case (Var type val) with assms have "varType_inv type" by simp
with Var show ?thesis
by (cases idx)
(auto intro!: checkVarValue_Var
simp del: checkVarValue.simps variable_inv.simps)
next
case (VArray type siz vals)
with assms have [simp, intro!]: "varType_inv type" by simp
show ?thesis
proof (cases idx)
case None with assms VArray show ?thesis
by (cases "IArray.list_of vals") (auto intro!: checkVarValue_bounds)
next
case (Some i)
note upd_cases = in_set_upd_cases[where l="IArray.list_of vals" and i="nat_of_integer i"]
from Some VArray assms show ?thesis
by (cases type)
(auto elim!: upd_cases intro!: mod_integer_le mod_integer_ge simp add: min_var_value_def)
qed
qed
definition getVar'
:: "bool ⇒ String.literal ⇒ integer option
⇒ 'a gState_scheme ⇒ pState
⇒ integer option"
where
"getVar' gl v idx g p = (
let vars = if gl then gState.vars g else pState.vars p in
map_option (λx. lookupVar x idx) (lm.lookup v vars))"
definition setVar'
:: "bool ⇒ String.literal ⇒ integer option
⇒ integer
⇒ 'a gState_scheme ⇒ pState
⇒ 'a gState_scheme * pState"
where
"setVar' gl v idx val g p = (
if gl then
if v = STR ''_'' then (g,p)
else case lm.lookup v (gState.vars g) of
None ⇒ abortv STR ''Unknown global variable: '' v (λ_. (g,p))
| Some x ⇒ (g⦇gState.vars := lm.update v (editVar x idx val)
(gState.vars g)⦈
, p)
else
case lm.lookup v (pState.vars p) of
None ⇒ abortv STR ''Unknown proc variable: '' v (λ_. (g,p))
| Some x ⇒ (g, p⦇pState.vars := lm.update v (editVar x idx val)
(pState.vars p)⦈))"
lemma setVar'_gState_inv:
assumes "gState_inv prog g"
shows "gState_inv prog (fst (setVar' gl v idx val g p))"
unfolding setVar'_def using assms
by (auto simp add: gState_inv_def lm.correct
intro: editVar_variable_inv
split: option.splits)
lemma setVar'_gState_progress_rel:
assumes "gState_inv prog g"
shows "(g, fst (setVar' gl v idx val g p)) ∈ gState_progress_rel prog"
apply (intro gState_progress_relI)
apply (fact assms)
apply (fact setVar'_gState_inv[OF assms])
apply (auto simp: setVar'_def lm.correct split: option.splits)
done
lemma vardict_inv_process_names:
assumes "vardict_inv ss proc v"
and "lm.lookup k v = Some x"
shows "k ∈ process_names ss proc"
using assms
by (auto simp add: lm.correct vardict_inv_def)
lemma vardict_inv_variable_inv:
assumes "vardict_inv ss proc v"
and "lm.lookup k v = Some x"
shows "variable_inv x"
using assms
by (auto simp add: lm.correct vardict_inv_def)
lemma vardict_inv_updateI:
assumes "vardict_inv ss proc vs"
and "x ∈ process_names ss proc"
and "variable_inv v"
shows "vardict_inv ss proc (lm.update x v vs)"
using assms
by (auto simp add: lm.correct vardict_inv_def)
lemma update_vardict_inv:
assumes "vardict_inv ss proc v"
and "lm.lookup k v = Some x"
and "variable_inv x'"
shows "vardict_inv ss proc (lm.update k x' v)"
using assms
by (auto intro!: vardict_inv_updateI vardict_inv_process_names)
lemma setVar'_pState_inv:
assumes "pState_inv prog p"
shows "pState_inv prog (snd (setVar' gl v idx val g p))"
unfolding setVar'_def using assms
by (auto split: if_splits option.splits
simp add: pState_inv_def
intro: update_vardict_inv editVar_variable_inv vardict_inv_variable_inv)
lemma setVar'_cl_inv:
assumes "cl_inv (g,p)"
shows "cl_inv (setVar' gl v idx val g p)"
unfolding setVar'_def using assms
by (auto split: if_splits option.splits)
definition withVar'
:: "bool ⇒ String.literal ⇒ integer option
⇒ (integer ⇒ 'x)
⇒ 'a gState_scheme ⇒ pState
⇒ 'x"
where
"withVar' gl v idx f g p = f (the (getVar' gl v idx g p))"
definition withChannel'
:: "bool ⇒ String.literal ⇒ integer option
⇒ (nat ⇒ channel ⇒ 'x)
⇒ 'a gState_scheme ⇒ pState
⇒ 'x"
where
"withChannel' gl v idx f g p = (
let error = λ_. abortv STR ''Variable is not a channel: '' v
(λ_. f 0 InvChannel) in
let abort = λ_. abortv STR ''Channel already closed / invalid: '' v
(λ_. f 0 InvChannel)
in withVar' gl v idx (λi. let i = nat_of_integer i in
if i ≥ length (channels g) then error ()
else let c = channels g ! i in
case c of
InvChannel ⇒ abort ()
| _ ⇒ f i c) g p)"
subsection ‹Expressions›
text ‹Expressions are free of side-effects.
This is in difference to SPIN, where @{term run} is an expression with side-effect. We treat @{term run} as a statement.›
abbreviation "trivCond x ≡ if x then 1 else 0"
fun exprArith :: "'a gState_scheme ⇒ pState ⇒ expr ⇒ integer"
and pollCheck :: "'a gState_scheme ⇒ pState ⇒ channel ⇒ recvArg list ⇒ bool
⇒ bool"
and recvArgsCheck :: "'a gState_scheme ⇒ pState ⇒ recvArg list ⇒ integer list
⇒ bool"
where
"exprArith g p (ExprConst x) = x"
| "exprArith g p (ExprMConst x _) = x"
| "exprArith g p ExprTimeOut = trivCond (timeout g)"
| "exprArith g p (ExprLen (ChanRef (VarRef gl name None))) =
withChannel' gl name None (
λ_ c. case c of
Channel _ _ q ⇒ integer_of_nat (length q)
| HSChannel _ ⇒ 0) g p"
| "exprArith g p (ExprLen (ChanRef (VarRef gl name (Some idx)))) =
withChannel' gl name (Some (exprArith g p idx)) (
λ_ c. case c of
Channel _ _ q ⇒ integer_of_nat (length q)
| HSChannel _ ⇒ 0) g p"
| "exprArith g p (ExprEmpty (ChanRef (VarRef gl name None))) =
trivCond (withChannel' gl name None (
λ_ c. case c of Channel _ _ q ⇒ (q = [])
| HSChannel _ ⇒ True) g p)"
| "exprArith g p (ExprEmpty (ChanRef (VarRef gl name (Some idx)))) =
trivCond (withChannel' gl name (Some (exprArith g p idx)) (
λ_ c. case c of Channel _ _ q ⇒ (q = [])
| HSChannel _ ⇒ True) g p)"
| "exprArith g p (ExprFull (ChanRef(VarRef gl name None))) =
trivCond (withChannel' gl name None (
λ_ c. case c of
Channel cap _ q ⇒ integer_of_nat (length q) ≥ cap
| HSChannel _ ⇒ False) g p)"
| "exprArith g p (ExprFull (ChanRef(VarRef gl name (Some idx)))) =
trivCond (withChannel' gl name (Some (exprArith g p idx)) (
λ_ c. case c of
Channel cap _ q ⇒ integer_of_nat (length q) ≥ cap
| HSChannel _ ⇒ False) g p)"
| "exprArith g p (ExprVarRef (VarRef gl name None)) =
withVar' gl name None id g p"
| "exprArith g p (ExprVarRef (VarRef gl name (Some idx))) =
withVar' gl name (Some (exprArith g p idx)) id g p"
| "exprArith g p (ExprUnOp UnOpMinus expr) = 0 - exprArith g p expr"
| "exprArith g p (ExprUnOp UnOpNeg expr) = ((exprArith g p expr) + 1) mod 2"
| "exprArith g p (ExprBinOp BinOpAdd lexpr rexpr) =
(exprArith g p lexpr) + (exprArith g p rexpr)"
| "exprArith g p (ExprBinOp BinOpSub lexpr rexpr) =
(exprArith g p lexpr) - (exprArith g p rexpr)"
| "exprArith g p (ExprBinOp BinOpMul lexpr rexpr) =
(exprArith g p lexpr) * (exprArith g p rexpr)"
| "exprArith g p (ExprBinOp BinOpDiv lexpr rexpr) =
(exprArith g p lexpr) div (exprArith g p rexpr)"
| "exprArith g p (ExprBinOp BinOpMod lexpr rexpr) =
(exprArith g p lexpr) mod (exprArith g p rexpr)"
| "exprArith g p (ExprBinOp BinOpGr lexpr rexpr) =
trivCond (exprArith g p lexpr > exprArith g p rexpr)"
| "exprArith g p (ExprBinOp BinOpLe lexpr rexpr) =
trivCond (exprArith g p lexpr < exprArith g p rexpr)"
| "exprArith g p (ExprBinOp BinOpGEq lexpr rexpr) =
trivCond (exprArith g p lexpr ≥ exprArith g p rexpr)"
| "exprArith g p (ExprBinOp BinOpLEq lexpr rexpr) =
trivCond (exprArith g p lexpr ≤ exprArith g p rexpr)"
| "exprArith g p (ExprBinOp BinOpEq lexpr rexpr) =
trivCond (exprArith g p lexpr = exprArith g p rexpr)"
| "exprArith g p (ExprBinOp BinOpNEq lexpr rexpr) =
trivCond (exprArith g p lexpr ≠ exprArith g p rexpr)"
| "exprArith g p (ExprBinOp BinOpAnd lexpr rexpr) =
trivCond (exprArith g p lexpr ≠ 0 ∧ exprArith g p rexpr ≠ 0)"
| "exprArith g p (ExprBinOp BinOpOr lexpr rexpr) =
trivCond (exprArith g p lexpr ≠ 0 ∨ exprArith g p rexpr ≠ 0)"
| "exprArith g p (ExprCond cexpr texpr fexpr) =
(if exprArith g p cexpr ≠ 0 then exprArith g p texpr
else exprArith g p fexpr)"
| "exprArith g p (ExprPoll (ChanRef (VarRef gl name None)) rs srt) =
trivCond (withChannel' gl name None (
λ_ c. pollCheck g p c rs srt) g p)"
| "exprArith g p (ExprPoll (ChanRef (VarRef gl name (Some idx))) rs srt) =
trivCond (withChannel' gl name (Some (exprArith g p idx)) (
λ_ c. pollCheck g p c rs srt) g p)"
| "pollCheck g p InvChannel _ _ =
abort STR ''Channel already closed / invalid.'' (λ_. False)"
| "pollCheck g p (HSChannel _) _ _ = False"
| "pollCheck g p (Channel _ _ q) rs srt = (
if q = [] then False
else if ¬ srt then recvArgsCheck g p rs (hd q)
else List.find (recvArgsCheck g p rs) q ≠ None)"
| "recvArgsCheck _ _ [] [] = True"
| "recvArgsCheck _ _ _ [] =
abort STR ''Length mismatch on receiving.'' (λ_. False)"
| "recvArgsCheck _ _ [] _ =
abort STR ''Length mismatch on receiving.'' (λ_. False)"
| "recvArgsCheck g p (r#rs) (v#vs) = ((
case r of
RecvArgConst c ⇒ c = v
| RecvArgMConst c _ ⇒ c = v
| RecvArgVar var ⇒ True
| RecvArgEval e ⇒ exprArith g p e = v ) ∧ recvArgsCheck g p rs vs)"
text ‹@{const getVar'} etc.\ do operate on name, index, \ldots directly. Lift them to use @{const VarRef} instead.›
fun liftVar where
"liftVar f (VarRef gl v idx) argm g p =
f gl v (map_option (exprArith g p) idx) argm g p"
definition "getVar v = liftVar (λgl v idx arg. getVar' gl v idx) v ()"
definition "setVar = liftVar setVar'"
definition "withVar = liftVar withVar'"
primrec withChannel
where "withChannel (ChanRef v) = liftVar withChannel' v"
lemma setVar_gState_progress_rel:
assumes "gState_inv prog g"
shows "(g, fst (setVar v val g p)) ∈ gState_progress_rel prog"
unfolding setVar_def
by (cases v) (simp add: setVar'_gState_progress_rel[OF assms])
lemmas setVar_gState_inv =
setVar_gState_progress_rel[THEN gState_progress_rel_gState_invI2]
lemma setVar_pState_inv:
assumes "pState_inv prog p"
shows "pState_inv prog (snd (setVar v val g p))"
unfolding setVar_def
by (cases v) (auto simp add: setVar'_pState_inv assms)
lemma setVar_cl_inv:
assumes "cl_inv (g,p)"
shows "cl_inv (setVar v val g p)"
unfolding setVar_def
by (cases v) (auto simp add: setVar'_cl_inv assms)
subsection ‹Variable declaration›
lemma channel_inv_code [code]:
"channel_inv (Channel cap ts q)
⟷ cap ≤ max_array_size
∧ 0 ≤ cap
∧ for_all varType_inv ts
∧ length ts ≤ max_array_size
∧ length q ≤ max_array_size
∧ for_all (λx. length x = length ts
∧ for_all (λy. y ≥ min_var_value
∧ y ≤ max_var_value) x) q"
"channel_inv (HSChannel ts)
⟷ for_all varType_inv ts ∧ length ts ≤ max_array_size"
by (auto simp add: for_all_def) force+
primrec toVariable
:: "'a gState_scheme ⇒ pState ⇒ varDecl ⇒ String.literal * variable * channels"
where
"toVariable g p (VarDeclNum lb hb name siz init) = (
let type = VTBounded lb hb in
if ¬ varType_inv type then abortv STR ''Invalid var def (varType_inv failed): '' name
(λ_. (name, Var VTChan 0, []))
else
let
init = checkVarValue type (case init of
None ⇒ 0
| Some e ⇒ exprArith g p e);
v = (case siz of
None ⇒ Var type init
| Some s ⇒ if nat_of_integer s ≤ max_array_size
then VArray type (nat_of_integer s)
(IArray.tabulate (s, λ_. init))
else abortv STR ''Invalid var def (array too large): '' name
(λ_. Var VTChan 0))
in
(name, v, []))"
| "toVariable g p (VarDeclChan name siz types) = (
let
size = (case siz of None ⇒ 1 | Some s ⇒ nat_of_integer s);
chans = (case types of
None ⇒ []
| Some (cap, tys) ⇒
let C = (if cap = 0 then HSChannel tys
else Channel cap tys []) in
if ¬ channel_inv C
then abortv STR ''Invalid var def (channel_inv failed): ''
name (λ_. [])
else replicate size C);
cidx = (case types of
None ⇒ 0
| Some _ ⇒ integer_of_nat (length (channels g)));
v = (case siz of
None ⇒ Var VTChan cidx
| Some s ⇒ if nat_of_integer s ≤ max_array_size
then VArray VTChan (nat_of_integer s)
(IArray.tabulate (s,
λi. if cidx = 0 then 0
else i + cidx))
else abortv STR ''Invalid var def (array too large): ''
name (λ_. Var VTChan 0))
in
(name, v, chans))"
lemma toVariable_variable_inv:
assumes "gState_inv prog g"
shows "variable_inv (fst (snd (toVariable g p v)))"
using assms
apply (cases v)
apply (auto intro!: checkVarValue_Var
simp del: variable_inv.simps checkVarValue.simps varType_inv.simps
split: if_splits option.splits)
apply (auto intro!: mod_integer_ge mod_integer_le simp add: min_var_value_def)
apply (simp_all add: assms gState_inv_def
max_channels_def max_var_value_def min_var_value_def max_array_size_def)
including integer.lifting
apply (transfer', simp)+
done
lemma toVariable_channels_inv:
shows "∀x ∈ set (snd (snd (toVariable g p v))). channel_inv x"
by (cases v) auto
lemma toVariable_channels_inv':
shows "toVariable g p v = (a,b,c) ⟹ ∀x ∈ set c. channel_inv x"
using toVariable_channels_inv
by (metis snd_conv)
lemma toVariable_variable_inv':
shows "gState_inv prog g ⟹ toVariable g p v = (a,b,c) ⟹ variable_inv b"
by (metis snd_conv fst_conv toVariable_variable_inv)
definition mkChannels
:: "'a gState_scheme ⇒ pState ⇒ channels ⇒ 'a gState_scheme * pState"
where
"mkChannels g p cs = (
if cs = [] then (g,p) else
let l = length (channels g) in
if l + length cs > max_channels
then abort STR ''Too much channels'' (λ_. (g,p))
else let
cs⇩p = map integer_of_nat [l..<l + length cs];
g' = g⦇channels := channels g @ cs⦈;
p' = p⦇pState.channels := pState.channels p @ cs⇩p⦈
in
(g', p'))"
lemma mkChannels_gState_progress_rel:
"gState_inv prog g
⟹ set cs ⊆ Collect channel_inv
⟹ (g, fst (mkChannels g p cs)) ∈ gState_progress_rel prog"
unfolding mkChannels_def
by (intro gState_progress_relI)
(auto simp add: gState_inv_def gState.defs cl_inv_def)
lemmas mkChannels_gState_inv =
mkChannels_gState_progress_rel[THEN gState_progress_rel_gState_invI2]
lemma mkChannels_pState_inv:
"pState_inv prog p
⟹ cl_inv (g,p)
⟹ pState_inv prog (snd (mkChannels g p cs))"
unfolding mkChannels_def
including integer.lifting
apply (auto simp add: pState_inv_def pState.defs gState_inv_def dest!: cl_inv_lengthD)
apply (transfer', simp)+
done
lemma mkChannels_cl_inv:
"cl_inv (g,p) ⟹ cl_inv (mkChannels g p cs)"
unfolding mkChannels_def
by (auto simp add: pState.defs dest: cl_inv_lengthD intro!: cl_invI)
definition mkVarChannel
:: "varDecl
⇒ ((var_dict ⇒ var_dict) ⇒ 'a gState_scheme * pState
⇒ 'a gState_scheme * pState)
⇒ 'a gState_scheme ⇒ pState
⇒ 'a gState_scheme * pState"
where
"mkVarChannel v upd g p = (
let
(k,v,cs) = toVariable g p v;
(g',p') = upd (lm.update k v) (g,p)
in
mkChannels g' p' cs)"
lemma mkVarChannel_gState_inv:
assumes "gState_inv prog g"
and "⋀k v' cs. toVariable g p v = (k,v',cs)
⟹ gState_inv prog (fst (upd (lm.update k v') (g,p)))"
shows "gState_inv prog (fst (mkVarChannel v upd g p))"
using assms unfolding mkVarChannel_def
by (force split: varDecl.split prod.split
intro!: mkChannels_gState_inv
dest: toVariable_channels_inv')
lemma mkVarChannel_gState_progress_rel:
assumes "gState_inv prog g"
and "⋀k v' cs. toVariable g p v = (k,v',cs)
⟹ (g, fst (upd (lm.update k v') (g,p))) ∈ gState_progress_rel prog"
shows "(g, fst (mkVarChannel v upd g p)) ∈ gState_progress_rel prog"
proof -
obtain k v' cs where 1: "toVariable g p v = (k,v',cs)" by (metis prod.exhaust)
obtain g' p' where 2: "(g',p') = upd (lm.update k v') (g,p)" by (metis prod.exhaust)
with 1 assms have *: "(g, g') ∈ gState_progress_rel prog" by (metis fst_conv)
also from 1 2 have "(g', fst (mkChannels g' p' cs)) ∈ gState_progress_rel prog"
by (force intro!: mkChannels_gState_progress_rel gState_progress_rel_gState_invI2[OF *]
dest: toVariable_channels_inv')
finally have "(g, fst (mkChannels g' p' cs)) ∈ gState_progress_rel prog" .
thus ?thesis using 1 2 by (auto simp add: mkVarChannel_def split: prod.split)
qed
lemma mkVarChannel_pState_inv:
assumes "pState_inv prog p"
and "cl_inv (g,p)"
and "⋀k v' cs. toVariable g p v = (k,v',cs)
⟹ cl_inv (upd (lm.update k v') (g,p))"
and "⋀k v' cs. toVariable g p v = (k,v',cs)
⟹ pState_inv prog (snd (upd (lm.update k v') (g,p)))"
shows "pState_inv prog (snd (mkVarChannel v upd g p))"
using assms unfolding mkVarChannel_def
by (force split: varDecl.split prod.split
intro!: mkChannels_pState_inv)
lemma mkVarChannel_cl_inv:
assumes "cl_inv (g,p)"
and "⋀k v' cs. toVariable g p v = (k,v',cs)
⟹ cl_inv (upd (lm.update k v') (g,p))"
shows "cl_inv (mkVarChannel v upd g p)"
using assms unfolding mkVarChannel_def
by (force split: varDecl.split prod.splits
intro!: mkChannels_cl_inv)
definition mkVarChannelProc
:: "procVarDecl ⇒ 'a gState_scheme ⇒ pState ⇒ 'a gState_scheme * pState"
where
"mkVarChannelProc v g p = (
let
v' = case v of
ProcVarDeclNum lb hb name siz init ⇒
VarDeclNum lb hb name siz init
| ProcVarDeclChan name siz ⇒
VarDeclChan name siz None;
(k,v,cs) = toVariable g p v'
in
mkVarChannel v' (apsnd ∘ pState.vars_update) g p)"
lemma mkVarChannelProc_gState_progress_rel:
assumes "gState_inv prog g"
shows "(g, fst (mkVarChannelProc v g p)) ∈ gState_progress_rel prog"
unfolding mkVarChannelProc_def
using assms
by (auto intro!: mkVarChannel_gState_progress_rel)
lemmas mkVarChannelProc_gState_inv =
mkVarChannelProc_gState_progress_rel[THEN gState_progress_rel_gState_invI2]
lemma toVariable_name:
"toVariable g p (VarDeclNum lb hb name sz init) = (x,a,b) ⟹ x = name"
"toVariable g p (VarDeclChan name sz t) = (x, a, b) ⟹ x = name"
by (auto split: if_splits)
declare toVariable.simps[simp del]
lemma statesDecls_process_names:
assumes "v ∈ statesDecls (states prog !! (pState.idx p))"
shows "procVarDeclName v ∈ process_names (states prog !! (pState.idx p))
(processes prog !! (pState.idx p))"
using assms
by (cases "processes prog !! (pState.idx p)") (auto simp add: statesNames_def)
lemma mkVarChannelProc_pState_inv:
assumes "pState_inv prog p"
and "gState_inv prog g"
and "cl_inv (g, p)"
and decl: "v ∈ statesDecls (states prog !! (pState.idx p))"
shows "pState_inv prog (snd (mkVarChannelProc v g p))"
unfolding mkVarChannelProc_def
using assms statesDecls_process_names[OF decl]
by (auto intro!: mkVarChannel_pState_inv)
(auto dest: toVariable_name
split: procVarDecl.splits
intro: toVariable_variable_inv' vardict_inv_updateI
simp add: pState_inv_def)
lemma mkVarChannelProc_cl_inv:
assumes "cl_inv (g,p)"
shows "cl_inv (mkVarChannelProc v g p)"
unfolding mkVarChannelProc_def using assms
by (auto intro!: mkVarChannel_cl_inv)
subsection ‹Folding›
text ‹
Fold over lists (and lists of lists) of @{typ step}/@{typ stmnt}. The folding functions are
doing a bit more than that, e.g.\ ensuring the offset into the program array is correct.
›
definition step_fold' where
"step_fold' g steps (lbls :: labels) pri pos
(nxt :: edgeIndex) (onxt :: edgeIndex option) iB =
foldr (λstep (pos, nxt, lbls, es).
let (e,enxt,lbls) = g step (lbls, pri, pos, nxt, onxt, iB)
in (pos + length e, enxt, lbls, es@e)
) steps (pos, nxt, lbls, [])"
definition step_fold where
"step_fold g steps lbls pri pos nxt onxt iB = (
let (_,nxt,lbls,s) = step_fold' g steps lbls pri pos nxt onxt iB
in (s,nxt,lbls))"
lemma step_fold'_cong:
assumes "lbls = lbls'"
and "pri = pri'"
and "pos = pos'"
and "steps = steps'"
and "nxt = nxt'"
and "onxt = onxt'"
and "iB = iB'"
and "⋀x d. x ∈ set steps ⟹ g x d = g' x d"
shows "step_fold' g steps lbls pri pos nxt onxt iB =
step_fold' g' steps' lbls' pri' pos' nxt' onxt' iB'"
unfolding step_fold'_def
by (auto intro: foldr_cong simp add: assms)
lemma step_fold_cong[fundef_cong]:
assumes "lbls = lbls'"
and "pri = pri'"
and "pos = pos'"
and "steps = steps'"
and "nxt = nxt'"
and "onxt = onxt'"
and "iB = iB'"
and "⋀x d. x ∈ set steps ⟹ g x d = g' x d"
shows "step_fold g steps lbls pri pos nxt onxt iB =
step_fold g' steps' lbls' pri' pos' nxt' onxt' iB'"
unfolding step_fold_def
by (auto simp: assms cong: step_fold'_cong)
fun step_foldL_step where
"step_foldL_step _ _ _ [] (pos, nxt, lbls, es, is) = (pos, nxt, lbls, es, is)"
| "step_foldL_step g pri onxt (s#steps) (pos, nxt, lbls, es, is) = (
let (pos', nxt', lbls', ss') = step_fold' g steps lbls pri pos nxt onxt False in
let (s', nxt'', lbls'') = g s (lbls',pri,pos',nxt',onxt,True) in
let rs = butlast s'; s'' = last s' in
(pos' + length rs, nxt, lbls'', es@ss'@rs, s''#is))"
definition step_foldL where
"step_foldL g stepss lbls pri pos nxt onxt =
foldr (step_foldL_step g pri onxt) stepss (pos,nxt,lbls,[],[])"
lemma step_foldL_step_cong:
assumes "pri = pri'"
and "onxt = onxt'"
and "s = s'"
and "d = d'"
and "⋀x d. x ∈ set s ⟹ g x d = g' x d"
shows "step_foldL_step g pri onxt s d = step_foldL_step g' pri' onxt' s' d'"
using assms
by (cases d', cases s') (simp_all cong: step_fold'_cong)
lemma step_foldL_cong[fundef_cong]:
assumes "lbls = lbls'"
and "pri = pri'"
and "pos = pos'"
and "stepss = stepss'"
and "nxt = nxt'"
and "onxt = onxt'"
and "⋀x x' d. x ∈ set stepss ⟹ x' ∈ set x ⟹ g x' d = g' x' d"
shows "step_foldL g stepss lbls pri pos nxt onxt =
step_foldL g' stepss' lbls' pri' pos' nxt' onxt'"
unfolding step_foldL_def
using assms
apply (cases stepss')
apply simp
apply (force intro!: foldr_cong step_foldL_step_cong)
done
subsection ‹Starting processes›
definition modProcArg
:: "(procArg * integer) ⇒ String.literal * variable"
where
"modProcArg x = (
case x of
(ProcArg ty name, val) ⇒ if varType_inv ty
then let init = checkVarValue ty val
in (name, Var ty init)
else abortv STR ''Invalid proc arg (varType_inv failed)''
name (λ_. (name, Var VTChan 0)))"
definition emptyProc :: "pState"
where
"emptyProc = ⦇pid = 0, vars = lm.empty (), pc = 0, channels = [], idx = 0 ⦈"
lemma vardict_inv_empty:
"vardict_inv ss proc (lm.empty())"
unfolding vardict_inv_def
by (simp add: lm.correct)
lemma emptyProc_cl_inv[simp]:
"cl_inv (g, emptyProc)"
by (simp add: cl_inv_def emptyProc_def)
lemma emptyProc_pState_inv:
assumes "program_inv prog"
shows "pState_inv prog emptyProc"
proof -
from assms have "IArray.length (states prog !! 0) > 0"
by (intro program_inv_length_states) (auto simp add: program_inv_def)
with assms show ?thesis
unfolding pState_inv_def program_inv_def emptyProc_def
by (auto simp add: vardict_inv_empty)
qed
fun mkProc
:: "'a gState_scheme ⇒ pState
⇒ String.literal ⇒ expr list ⇒ process ⇒ nat
⇒ 'a gState_scheme * pState"
where
"mkProc g p name args (sidx, start, argDecls, decls) pidN = (
let start = case start of
Index x ⇒ x
| _ ⇒ abortv STR ''Process start is not index: '' name (λ_. 0)
in
if length args ≠ length argDecls
then abortv STR ''Signature mismatch: '' name (λ_. (g,emptyProc))
else
let
eArgs = map (exprArith g p) args;
argVars = map modProcArg (zip argDecls eArgs);
pidI = integer_of_nat pidN;
argVars = (STR ''_pid'', Var (VTBounded 0 pidI) pidI)#argVars;
argVars = lm.to_map argVars;
p = ⦇ pid = pidN, vars = argVars, pc = start, channels = [], idx = sidx ⦈
in
foldl (λ(g,p) d. mkVarChannel d (apsnd ∘ pState.vars_update) g p)
(g,p)
decls)"
lemma mkProc_gState_progress_rel:
assumes "gState_inv prog g"
shows "(g, fst (mkProc g p name args (processes prog !! sidx) pidN)) ∈
gState_progress_rel prog"
proof -
obtain sidx' start argDecls decls where
p: "processes prog !! sidx = (sidx', start, argDecls, decls)"
by (metis prod.exhaust)
from assms have
"⋀p. (g, fst (foldl (λ(g,p) d. mkVarChannel d (apsnd ∘ pState.vars_update) g p)
(g,p) decls))
∈ gState_progress_rel prog"
proof (induction decls arbitrary: g p)
case (Cons d decls)
obtain g' p' where
new: "(g',p') = (mkVarChannel d (apsnd ∘ pState.vars_update) g p)"
by (metis prod.exhaust)
hence "g' = fst ..." by (metis fst_conv)
with Cons.prems have g_g': "(g,g') ∈ gState_progress_rel prog"
by (auto intro: mkVarChannel_gState_progress_rel)
also note Cons.IH[OF g_g'[THEN gState_progress_rel_gState_invI2], of p']
finally show ?case by (auto simp add: o_def new)
qed simp
thus ?thesis using assms p by auto
qed
lemmas mkProc_gState_inv =
mkProc_gState_progress_rel[THEN gState_progress_rel_gState_invI2]
lemma mkProc_pState_inv:
assumes "program_inv prog"
and "gState_inv prog g"
and "pidN ≤ max_procs" and "pidN > 0"
and "sidx < IArray.length (processes prog)"
and "fst (processes prog !! sidx) = sidx"
shows "pState_inv prog (snd (mkProc g p name args (processes prog !! sidx) pidN))"
proof -
obtain sidx' start argDecls decls where
"processes prog !! sidx = (sidx', start, argDecls, decls)"
by (metis prod.exhaust)
with assms have
p_def: "processes prog !! sidx = (sidx, start, argDecls, decls)"
"IArray.list_of (processes prog) ! sidx = (sidx, start, argDecls, decls)"
by simp_all
with assms have "(sidx,start,argDecls,decls) ∈ set (IArray.list_of (processes prog))"
by (force dest: nth_mem)
with assms obtain s where s: "start = Index s" "s < IArray.length (states prog !! sidx)"
unfolding program_inv_def by auto
hence P_inv: "pState_inv prog ⦇
pid = pidN,
vars = lm.to_map
((STR ''_pid'', Var (VTBounded 0 (integer_of_nat pidN))
(integer_of_nat pidN))
# map modProcArg (zip argDecls (map (exprArith g p) args))),
pc = s, channels = [], idx = sidx⦈"
unfolding pState_inv_def
using assms[unfolded program_inv_def]
including integer.lifting
apply (simp add: p_def)
apply (intro lm_to_map_vardict_inv)
apply auto
apply (simp add: max_procs_def max_var_value_def)
apply transfer'
apply simp
apply transfer'
apply simp
apply (simp add: min_var_value_def)
apply transfer'
apply simp
apply (simp add: max_var_value_def max_procs_def)
apply transfer'
apply simp
apply (drule set_zip_leftD)
apply (force simp add: modProcArg_def
split: procArg.splits if_splits
intro!: image_eqI)
apply (clarsimp simp add: modProcArg_def
split: procArg.splits if_splits
simp del: variable_inv.simps)
apply (intro checkVarValue_Var)
apply assumption
done
from p_def have
"varDeclName ` set decls ⊆
process_names (states prog !! sidx) (processes prog !! sidx)"
by auto
with ‹gState_inv prog g› have
F_inv: "⋀p. ⟦ pState_inv prog p; sidx = pState.idx p; cl_inv (g,p) ⟧
⟹ pState_inv prog
(snd (foldl (λ(g,p) d. mkVarChannel d (apsnd ∘ pState.vars_update) g p)
(g,p) decls))"
proof (induction decls arbitrary: g p)
case (Cons d ds) hence
decl: "varDeclName d ∈ process_names (states prog !! pState.idx p)
(processes prog !! pState.idx p)"
by simp
obtain g' p' where
new: "(g',p') = (mkVarChannel d (apsnd ∘ pState.vars_update) g p)"
by (metis prod.exhaust)
hence p': "p' = snd ..." and g': "g' = fst ..."
by (metis snd_conv fst_conv)+
with Cons.prems have "pState_inv prog p'"
apply (auto intro!: mkVarChannel_pState_inv)
apply (simp add: pState_inv_def)
apply (intro vardict_inv_updateI)
apply simp
apply (cases d)
apply (force dest!: toVariable_name)
apply (force dest!: toVariable_name)
apply (intro toVariable_variable_inv')
apply assumption+
done
moreover
from p' Cons.prems have "pState.idx p' = sidx"
by (auto simp add: mkVarChannel_def mkChannels_def split: prod.split)
moreover
from new Cons.prems have "cl_inv (g',p')"
by (auto intro!: mkVarChannel_cl_inv)
moreover
from g' Cons.prems have "gState_inv prog g'"
by (auto intro!: mkVarChannel_gState_inv)
moreover
from Cons.prems have
"varDeclName ` set ds ⊆
process_names (states prog !! sidx) (processes prog !! sidx)"
by simp
ultimately
have
"pState_inv prog
(snd (foldl (λ(g,p) d. mkVarChannel d (apsnd ∘ pState.vars_update) g p)
(g',p') ds))"
using Cons.IH[of p' g'] by (simp add: o_def)
with new show ?case by (simp add: o_def)
qed simp
show ?thesis
by (auto simp add: p_def s cl_inv_def
intro: F_inv[OF P_inv])
(blast intro: emptyProc_pState_inv assms)
qed
lemma mkProc_cl_inv:
assumes "cl_inv (g,p)"
shows "cl_inv (mkProc g p name args (processes prog !! sidx) pidN)"
proof -
note IArray.sub_def [simp del]
obtain sidx' start argDecls decls
where [simp]: "processes prog !! sidx = (sidx', start, argDecls, decls)"
by (metis prod.exhaust)
have
P_inv: "⋀s v. cl_inv (g, ⦇pid = pidN, vars = v, pc = s, channels = [], idx = sidx' ⦈)"
by (simp add: cl_inv_def)
have
"⋀p. cl_inv(g,p) ⟹
cl_inv (foldl (λ(g,p) d. mkVarChannel d (apsnd ∘ pState.vars_update) g p)
(g,p) decls)"
proof (induction decls arbitrary: g p)
case (Cons d ds)
obtain g' p' where
new: "(g',p') = (mkVarChannel d (apsnd ∘ pState.vars_update) g p)"
by (metis prod.exhaust)
with Cons.prems have "cl_inv (g',p')"
by (auto intro!: mkVarChannel_cl_inv)
from Cons.IH[OF this] new show ?case by (simp add: o_def)
qed simp
from this[OF P_inv] show ?thesis by auto
qed
declare mkProc.simps[simp del]
definition runProc
:: "String.literal ⇒ expr list ⇒ program
⇒ 'a gState_scheme ⇒ pState
⇒ 'a gState_scheme * pState"
where
"runProc name args prog g p = (
if length (procs g) ≥ max_procs
then abort STR ''Too many processes'' (λ_. (g,p))
else let pid = length (procs g) + 1 in
case lm.lookup name (proc_data prog) of
None ⇒ abortv STR ''No such process: '' name
(λ_. (g,p))
| Some proc_idx ⇒
let (g', proc) = mkProc g p name args (processes prog !! proc_idx) pid
in (g'⦇procs := procs g @ [proc]⦈, p))"
lemma runProc_gState_progress_rel:
assumes "program_inv prog"
and "gState_inv prog g"
and "pState_inv prog p"
and "cl_inv (g,p)"
shows "(g, fst (runProc name args prog g p)) ∈ gState_progress_rel prog"
proof (cases "length (procs g) < max_procs")
note IArray.sub_def [simp del]
case True thus ?thesis
proof (cases "lm.lookup name (proc_data prog)")
case (Some proc_idx)
hence *: "proc_idx < IArray.length (processes prog)"
"fst (processes prog !! proc_idx) = proc_idx"
using assms
by (simp_all add: lm.correct program_inv_def)
obtain g' p' where
new: "(g',p') = mkProc g p name args (processes prog !! proc_idx) (length (procs g) + 1)"
by (metis prod.exhaust)
hence g': "g' = fst ..." and p': "p' = snd ..."
by (metis snd_conv fst_conv)+
from assms g' have "(g, g') ∈ gState_progress_rel prog "
by (auto intro!: mkProc_gState_progress_rel)
moreover
from * assms True p' have "pState_inv prog p'"
by (auto intro!: mkProc_pState_inv)
moreover
from assms new have "cl_inv (g',p')"
by (auto intro!: mkProc_cl_inv)
ultimately show ?thesis
using True Some new assms
unfolding runProc_def gState_progress_rel_def
by (clarsimp split: prod.split)
(auto simp add: gState_inv_def cl_inv_def)
next
case None with assms show ?thesis by (auto simp add: runProc_def)
qed
next
case False with assms show ?thesis by (auto simp add: runProc_def)
qed
lemmas runProc_gState_inv =
runProc_gState_progress_rel[THEN gState_progress_rel_gState_invI2]
lemma runProc_pState_id:
"snd (runProc name args prog g p) = p"
unfolding runProc_def
by (auto split: if_splits split: option.split prod.split)
lemma runProc_pState_inv:
assumes "pState_inv prog p"
shows "pState_inv prog (snd (runProc name args prog g p))"
by (simp add: assms runProc_pState_id)
lemma runProc_cl_inv:
assumes "program_inv prog"
and "gState_inv prog g"
and "pState_inv prog p"
and "cl_inv (g,p)"
shows "cl_inv (runProc name args prog g p)"
proof -
obtain g' p' where *: "runProc name args prog g p = (g',p')"
by (metis prod.exhaust)
with runProc_gState_progress_rel[OF assms, of name args] have
"length (channels g) ≤ length (channels g')"
by (simp add: gState_progress_rel_def)
moreover from * runProc_pState_id have "p' = p" by (metis snd_conv)
ultimately show ?thesis by (metis ‹cl_inv (g,p)› * cl_inv_trans)
qed
subsection ‹AST to edges›
type_synonym ast = "AST.module list"
text ‹In this section, the AST is translated into the transition system.›
text ‹
Handling atomic blocks is non-trivial. Therefore, we do this in an extra pass:
@{term lp} and @{term hp} are the positions of the start and the end of
the atomic block. Every edge pointing into this range is therefore marked as
@{term Atomic}. If they are pointing somewhere else, they are set to @{term InAtomic},
meaning: they start \emph{in} an atomic block, but leave it afterwards.
›
definition atomize :: "nat ⇒ nat ⇒ edge list ⇒ edge list" where
"atomize lp hp es = fold (λe es.
let e' = case target e of
LabelJump _ None ⇒
e⦇ atomic := InAtomic ⦈
| LabelJump _ (Some via) ⇒
if lp ≤ via ∧ hp ≥ via then e⦇ atomic := Atomic ⦈
else e⦇ atomic := InAtomic ⦈
| Index p' ⇒
if lp ≤ p' ∧ hp ≥ p' then e⦇ atomic := Atomic ⦈
else e⦇ atomic := InAtomic ⦈
in e'#es) es []"
fun skip
where
"skip (lbls, pri, pos, nxt, _) =
([[⦇cond = ECExpr (ExprConst 1),
effect = EEId, target = nxt, prio = pri,
atomic = NonAtomic⦈]], Index pos, lbls)"
text ‹
The AST is walked backwards. This allows to know the next state directly.
Parameters used:
\begin{description}
\item[lbls] Map of Labels
\item[pri] Current priority
\item[pos] Current position in the array
\item[nxt] Next state
\item[onxt] Previous 'next state' (where to jump after a 'do')
\item[inBlock] Needed for certain constructs to calculate the layout of the array
\end{description}
›
fun stepToState
:: "step
⇒ (labels * integer * nat * edgeIndex * edgeIndex option * bool)
⇒ edge list list * edgeIndex * labels"
and stmntToState
:: "stmnt
⇒ (labels * integer * nat * edgeIndex * edgeIndex option * bool)
⇒ edge list list * edgeIndex * labels"
where
"stepToState (StepStmnt s None) data = stmntToState s data"
| "stepToState (StepStmnt s (Some u)) (lbls, pri, pos, nxt, onxt, _) = (
let
(ues,_,lbls') = stmntToState u (lbls, pri, pos, nxt, onxt, True);
u = last ues; ues = butlast ues;
pos' = pos + length ues;
pri = min_prio u pri;
(ses,spos,lbls'') = stmntToState s (lbls', pri - 1, pos', nxt, onxt, False);
ses = map (List.append u) ses
in
(ues@ses,spos,lbls''))"
| "stepToState (StepDecl decls) (lbls, pri, pos, nxt, onxt, _) = (
let edgeF = λd (lbls,pri,pos,nxt,_).
([[⦇cond = ECTrue, effect = EEDecl d, target = nxt,
prio = pri, atomic = NonAtomic⦈]], Index pos, lbls)
in
step_fold edgeF decls lbls pri pos nxt onxt False)"
| "stepToState StepSkip (lbls,_,_,nxt,_) = ([],nxt,lbls)"
| "stmntToState (StmntAtomic steps) (lbls, pri, pos, nxt, onxt, inBlock) = (
let (es,pos',lbls') = step_fold stepToState steps lbls pri pos nxt onxt inBlock in
let es' = map (atomize pos (pos + length es)) es in
(es', pos', lbls'))"
| "stmntToState (StmntLabeled l s) (lbls, pri, pos, d) = (
let
(es, pos', lbls) = stmntToState s (lbls, pri, pos, d);
lpos = case pos' of Index p ⇒ p | _ ⇒ pos;
lbls' = add_label l lbls lpos
in
(es, pos', lbls'))"
| "stmntToState (StmntDo stepss) (lbls, pri, pos, nxt, onxt, inBlock) = (
let
(_,_,lbls,es,is) = step_foldL stepToState stepss lbls pri
(pos+1) (Index pos) (Some nxt);
es' = concat is # es
in
if inBlock then
(es' @ [concat is], Index pos, lbls)
else
(es', Index pos, lbls)
)"
| "stmntToState (StmntIf stepss) (lbls, pri, pos, nxt, onxt, _) = (
let (pos,_,lbls,es,is) = step_foldL stepToState stepss lbls pri pos nxt onxt
in (es @ [concat is], Index pos, lbls))"
| "stmntToState (StmntSeq steps) (lbls, pri, pos, nxt, onxt, inBlock) =
step_fold stepToState steps lbls pri pos nxt onxt inBlock"
| "stmntToState (StmntAssign v e) (lbls, pri, pos, nxt, _) =
([[⦇cond = ECTrue, effect = EEAssign v e, target = nxt, prio = pri,
atomic = NonAtomic⦈]], Index pos, lbls)"
| "stmntToState (StmntAssert e) (lbls, pri, pos, nxt, _) =
([[⦇cond = ECTrue, effect = EEAssert e, target = nxt, prio = pri,
atomic = NonAtomic⦈]], Index pos, lbls)"
| "stmntToState (StmntCond e) (lbls, pri, pos, nxt, _) =
([[⦇cond = ECExpr e, effect = EEId, target = nxt, prio = pri,
atomic = NonAtomic⦈]], Index pos, lbls)"
| "stmntToState StmntElse (lbls, pri, pos, nxt, _) =
([[⦇cond = ECElse, effect = EEId, target = nxt, prio = pri,
atomic = NonAtomic ⦈]], Index pos, lbls)"
| "stmntToState StmntBreak (lbls,pri,_,_,Some onxt,_) =
([[⦇cond = ECTrue, effect = EEGoto, target = onxt, prio = pri,
atomic = NonAtomic ⦈]], onxt, lbls)"
| "stmntToState StmntBreak (_,_,_,_,None,_) =
abort STR ''Misplaced break'' (λ_. ([],Index 0,lm.empty()))"
| "stmntToState (StmntRun n args) (lbls, pri, pos, nxt, onxt, _) =
([[⦇cond = ECRun n, effect = EERun n args, target = nxt, prio = pri,
atomic = NonAtomic ⦈]], Index pos,lbls)"
| "stmntToState (StmntGoTo l) (lbls, pri, pos, _) =
([[⦇cond = ECTrue, effect = EEGoto, target = LabelJump l None, prio = pri,
atomic = NonAtomic ⦈]], LabelJump l (Some pos), lbls)"
| "stmntToState (StmntSend v e srt) (lbls, pri, pos, nxt, _) =
([[⦇cond = ECSend v, effect = EESend v e srt, target = nxt, prio = pri,
atomic = NonAtomic ⦈]], Index pos, lbls)"
| "stmntToState (StmntRecv v r srt rem) (lbls, pri, pos, nxt, _) =
([[⦇cond = ECRecv v r srt, effect = EERecv v r srt rem, target = nxt, prio = pri,
atomic = NonAtomic ⦈]], Index pos, lbls)"
| "stmntToState StmntSkip d = skip d"
subsubsection ‹Setup›
definition endState :: "edge list" where
"endState = [⦇ cond = ECFalse, effect = EEEnd, target = Index 0, prio = 0,
atomic = NonAtomic⦈]"
definition resolveLabel :: "String.literal ⇒ labels ⇒ nat" where
"resolveLabel l lbls = (
case lm.lookup l lbls of
None ⇒ abortv STR ''Unresolved label: '' l (λ_. 0)
| Some pos ⇒ pos)"
primrec resolveLabels :: "edge list list ⇒ labels ⇒ edge list ⇒ edge list" where
"resolveLabels _ _ [] = []"
| "resolveLabels edges lbls (e#es) = (
let check_atomic = λpos. fold (λe a. a ∧ inAtomic e) (edges ! pos) True in
case target e of
Index _ ⇒ e
| LabelJump l None ⇒
let pos = resolveLabel l lbls in
e⦇target := Index pos,
atomic := if inAtomic e then
if check_atomic pos then Atomic
else InAtomic
else NonAtomic ⦈
| LabelJump l (Some via) ⇒
let pos = resolveLabel l lbls in
e⦇target := Index pos,
atomic := if isAtomic e then
if check_atomic pos ∧ check_atomic via then Atomic
else InAtomic
else atomic e ⦈
) # (resolveLabels edges lbls es)"
definition calculatePrios :: "edge list list ⇒ (integer * edge list) list" where
"calculatePrios ess = map (λes. (min_prio es 0, es)) ess"
definition toStates :: "step list ⇒ states * edgeIndex * labels" where
"toStates steps = (
let
(states,pos,lbls) = step_fold stepToState steps (lm.empty())
0 1 (Index 0) None False;
pos = (case pos of
Index _ ⇒ pos
| LabelJump l _ ⇒ Index (resolveLabel l lbls));
states = endState # states;
states = map (resolveLabels states lbls) states;
states = calculatePrios states
in
case pos of Index s ⇒
if s < length states then (IArray states, pos, lbls)
else abort STR ''Start index out of bounds'' (λ_. (IArray states, Index 0, lbls)))"
lemma toStates_inv:
assumes "toStates steps = (ss,start,lbls)"
shows "∃s. start = Index s ∧ s < IArray.length ss"
and "IArray.length ss > 0"
using assms
unfolding toStates_def calculatePrios_def
by (auto split: prod.splits edgeIndex.splits if_splits)
primrec toProcess
:: "nat ⇒ proc ⇒ states * nat * String.literal * (labels * process)"
where
"toProcess sidx (ProcType act name args decls steps) = (
let
(states, start, lbls) = toStates steps;
act = (case act of
None ⇒ 0
| Some None ⇒ 1
| Some (Some x) ⇒ nat_of_integer x)
in
(states, act, name, lbls, sidx, start, args, decls))"
| "toProcess sidx (Init decls steps) = (
let (states, start, lbls) = toStates steps in
(states, 1, STR '':init:'', lbls, sidx, start, [], decls))"
lemma toProcess_sidx:
"toProcess sidx p = (ss,a,n,l,idx,r) ⟹ idx = sidx"
by (cases p) (simp_all split: prod.splits)
lemma toProcess_states_nonempty:
"toProcess sidx p = (ss,a,n,l,idx,r) ⟹ IArray.length ss > 0"
by (cases p) (force split: prod.splits dest: toStates_inv(2))+
lemma toProcess_start:
"toProcess sidx p = (ss,a,n,l,idx,start,r)
⟹ ∃s. start = Index s ∧ s < IArray.length ss"
by (cases p) (force split: prod.splits dest: toStates_inv(1))+
lemma toProcess_startE:
assumes "toProcess sidx p = (ss,a,n,l,idx,start,r)"
obtains s where "start = Index s" "s < IArray.length ss"
using toProcess_start[OF assms]
by blast
text ‹
The main construction function. Takes an AST
and returns an initial state,
and the program (= transition system).
›
definition setUp :: "ast ⇒ program × gState" where
"setUp ast = (
let
(decls, procs, _) = preprocess ast;
assertVar = Var (VTBounded 0 1) 0;
pre_procs = map (case_prod toProcess) (List.enumerate 1 procs);
procs = IArray ((0, Index 0, [], []) # map (λ(_,_,_,_,p). p) pre_procs);
labels = IArray (lm.empty() # map (λ(_,_,_,l,_). l) pre_procs);
states = IArray (IArray [(0,[])] # map (λ(s,_). s) pre_procs);
names = IArray (STR ''invalid'' # map (λ(_,_,n,_). n) pre_procs);
proc_data = lm.to_map (map (λ(_,_,n,_,idx,_). (n,idx)) pre_procs);
prog = ⦇ processes = procs, labels = labels, states = states,
proc_names = names, proc_data = proc_data ⦈;
g = ⦇ vars = lm.sng (STR ''__assert__'') assertVar,
channels = [InvChannel], timeout = False, procs = [] ⦈;
g' = foldl (λg d.
fst (mkVarChannel d (apfst ∘ gState.vars_update) g emptyProc)
) g decls;
g'' = foldl (λg (_,a,name,_).
foldl (λg name.
fst (runProc name [] prog g emptyProc)
) g (replicate a name)
) g' pre_procs
in
(prog, g''))"
lemma setUp_program_inv':
"program_inv (fst (setUp ast))"
proof (rule program_invI, goal_cases)
case 1 show ?case by (simp add: setUp_def split: prod.split)
next
case 2 show ?case by (simp add: setUp_def split: prod.split)
next
case 3 thus ?case
by (auto simp add: setUp_def o_def
split: prod.splits
dest!: toProcess_states_nonempty)
next
case 4 thus ?case
unfolding setUp_def
by (auto simp add: lm.correct o_def in_set_enumerate_eq nth_enumerate_eq
dest!: subsetD[OF Misc.ran_map_of] toProcess_sidx
split: prod.splits)
next
case 5 thus ?case
apply (auto simp add: setUp_def o_def split: prod.splits)
apply (frule toProcess_sidx)
apply (frule toProcess_start)
apply (auto simp: in_set_enumerate_eq nth_enumerate_eq)
done
qed
lemma setUp_program_inv:
assumes "setUp ast = (prog,g)"
shows "program_inv prog"
using assms setUp_program_inv'
by (metis fst_conv)
lemma setUp_gState_inv:
assumes "setUp ast = (prog, g)"
shows "gState_inv prog g"
proof -
from assms have p_INV: "program_inv prog" by (fact setUp_program_inv)
{
fix prog :: program
assume *: "program_inv prog"
let ?g = "⦇ vars = lm.sng (STR ''__assert__'') (Var (VTBounded 0 1) 0),
channels = [InvChannel], timeout = False, procs = [] ⦈"
have g1: "gState_inv prog ?g"
by (simp add: gState_inv_def max_channels_def lm_correct max_var_value_def)
{
fix g decls
assume "gState_inv prog g"
hence "gState_inv prog (foldl (λg d.
fst (mkVarChannel d (apfst ∘ gState.vars_update) g emptyProc)
) g decls)"
apply (rule foldl_rule)
apply (intro mkVarChannel_gState_inv)
apply simp
apply (frule_tac g=σ in toVariable_variable_inv')
apply assumption
apply (auto simp add: gState_inv_def lm.correct)
done
}
note g2 = this[OF g1]
{
fix g :: "'a gState_scheme" and pre_procs
assume "gState_inv prog g"
hence "gState_inv prog (foldl (λg (_,a,name,_).
foldl (λg name.
fst (runProc name [] prog g emptyProc)
) g (replicate a name)
) g pre_procs)"
apply (rule foldl_rule)
apply (clarsimp split: prod.splits)
apply (rule foldl_rule)
apply (auto intro!: runProc_gState_inv emptyProc_pState_inv *)
done
}
note this[OF g2]
} note g_INV = this
from assms p_INV show ?thesis
unfolding setUp_def
by (auto split: prod.splits intro!: g_INV)
qed
subsection ‹Semantic Engine›
text ‹
After constructing the transition system, we are missing the final part:
The successor function on this system. We use SPIN-nomenclature and call it
\emph{semantic engine}.
›
definition "assertVar ≡ VarRef True (STR ''__assert__'') None"
subsubsection ‹Evaluation of Edges›
fun evalRecvArgs
:: "recvArg list ⇒ integer list ⇒ gState⇩I ⇒ pState ⇒ gState⇩I * pState"
where
"evalRecvArgs [] [] g l = (g,l)"
| "evalRecvArgs _ [] g l =
abort STR ''Length mismatch on receiving.'' (λ_. (g,l))"
| "evalRecvArgs [] _ g l =
abort STR ''Length mismatch on receiving.'' (λ_. (g,l))"
| "evalRecvArgs (r#rs) (v#vs) g l = (
let (g,l) =
case r of
RecvArgVar var ⇒ setVar var v g l
| _ ⇒ (g,l)
in evalRecvArgs rs vs g l)"
primrec evalCond
:: "edgeCond ⇒ gState⇩I ⇒ pState ⇒ bool"
where
"evalCond ECTrue _ _ ⟷ True"
| "evalCond ECFalse _ _ ⟷ False"
| "evalCond (ECExpr e) g l ⟷ exprArith g l e ≠ 0"
| "evalCond (ECRun _) g l ⟷ length (procs g) < 255"
| "evalCond ECElse g l ⟷ gState⇩I.else g"
| "evalCond (ECSend v) g l ⟷
withChannel v (λ_ c.
case c of
Channel cap _ q ⇒ integer_of_nat (length q) < cap
| HSChannel _ ⇒ True) g l"
| "evalCond (ECRecv v rs srt) g l ⟷
withChannel v (λi c.
case c of
HSChannel _ ⇒ handshake g ≠ 0 ∧ recvArgsCheck g l rs (hsdata g)
| _ ⇒ pollCheck g l c rs srt) g l"
fun evalHandshake
:: "edgeCond ⇒ nat ⇒ gState⇩I ⇒ pState ⇒ bool"
where
"evalHandshake (ECRecv v _ _) h g l
⟷ h = 0
∨ withChannel v (λi c. case c of
HSChannel _ ⇒ i = h
| Channel _ _ _ ⇒ False) g l"
| "evalHandshake _ h _ _ ⟷ h = 0"
primrec evalEffect
:: "edgeEffect ⇒ program ⇒ gState⇩I ⇒ pState ⇒ gState⇩I * pState"
where
"evalEffect EEEnd _ g l = (g,l)"
| "evalEffect EEId _ g l = (g,l)"
| "evalEffect EEGoto _ g l = (g,l)"
| "evalEffect (EEAssign v e) _ g l = setVar v (exprArith g l e) g l"
| "evalEffect (EEDecl d) _ g l = mkVarChannelProc d g l"
| "evalEffect (EERun name args) prog g l = runProc name args prog g l"
| "evalEffect (EEAssert e) _ g l = (
if exprArith g l e = 0
then setVar assertVar 1 g l
else (g,l))"
| "evalEffect (EESend v es srt) _ g l = withChannel v (λi c.
let
ab = λ_. abort STR ''Length mismatch on sending.'' (λ_. (g,l));
es = map (exprArith g l) es
in
if ¬ for_all (λx. x ≥ min_var_value ∧ x ≤ max_var_value) es
then abort STR ''Invalid Channel'' (λ_. (g,l))
else
case c of
Channel cap ts q ⇒
if length ts ≠ length es ∨ ¬ (length q < max_array_size)
then ab()
else let
q' = if ¬ srt then q@[es]
else let
q = map lexlist q;
q' = insort (lexlist es) q
in map unlex q';
g = gState.channels_update (λcs.
cs[ i := Channel cap ts q' ]) g
in (g,l)
| HSChannel ts ⇒
if length ts ≠ length es then ab()
else (g⦇hsdata := es, handshake := i⦈, l)
| InvChannel ⇒ abort STR ''Trying to send on invalid channel'' (λ_. (g,l))
) g l"
| "evalEffect (EERecv v rs srt rem) _ g l = withChannel v (λi c.
case c of
Channel cap ts qs ⇒
if qs = [] then abort STR ''Recv from empty channel'' (λ_. (g,l))
else
let
(q', qs') = if ¬ srt then (hd qs, tl qs)
else apfst the (find_remove (recvArgsCheck g l rs) qs);
(g,l) = evalRecvArgs rs q' g l;
g = if rem
then gState.channels_update (λcs. cs[ i := Channel cap ts qs']) g
else g
in (g,l)
| HSChannel _ ⇒
let (g,l) = evalRecvArgs rs (hsdata g) g l in
let g = g⦇ handshake := 0, hsdata := [] ⦈
in (g,l)
| InvChannel ⇒ abort STR ''Receiving on invalid channel'' (λ_. (g,l))
) g l"
lemma statesDecls_effect:
assumes "ef ∈ effect ` edgeSet ss"
and "ef = EEDecl d"
shows "d ∈ statesDecls ss"
proof -
from assms obtain e where "e ∈ edgeSet ss" "ef = effect e" by auto
thus ?thesis using assms
unfolding statesDecls_def
by (auto simp add: edgeDecls_def
intro!: bexI[where x = e]
split: edgeEffect.split)
qed
lemma evalRecvArgs_pState_inv:
assumes "pState_inv prog p"
shows "pState_inv prog (snd (evalRecvArgs rargs xs g p))"
using assms
proof (induction rargs xs arbitrary: p g rule: list_induct2')
case (4 r rs x xs) thus ?case
proof (cases r)
case (RecvArgVar v)
obtain g' p' where new: "setVar v x g p = (g',p')" by (metis prod.exhaust)
hence "p' = snd (setVar v x g p)" by simp
with "4" have "pState_inv prog p'" by (auto intro!: setVar_pState_inv)
from "4.IH"[OF this] RecvArgVar new show ?thesis by simp
qed simp_all
qed simp_all
lemma evalRecvArgs_pState_inv':
assumes "evalRecvArgs rargs xs g p = (g', p')"
and "pState_inv prog p"
shows "pState_inv prog p'"
using assms evalRecvArgs_pState_inv
by (metis snd_conv)
lemma evalRecvArgs_gState_progress_rel:
assumes "gState_inv prog g"
shows "(g, fst (evalRecvArgs rargs xs g p)) ∈ gState_progress_rel prog"
using assms
proof (induction rargs xs arbitrary: p g rule: list_induct2')
case (4 r rs x xs) thus ?case
proof (cases r)
case (RecvArgVar v)
obtain g' p' where new: "setVar v x g p = (g',p')" by (metis prod.exhaust)
hence "g' = fst (setVar v x g p)" by simp
with "4" have "(g, g') ∈ gState_progress_rel prog"
by (auto intro!: setVar_gState_progress_rel)
also hence "gState_inv prog g'"
by (rule gState_progress_rel_gState_invI2)
note "4.IH"[OF this, of p']
finally show ?thesis using RecvArgVar new by simp
qed simp_all
qed simp_all
lemmas evalRecvArgs_gState_inv =
evalRecvArgs_gState_progress_rel[THEN gState_progress_rel_gState_invI2]
lemma evalRecvArgs_cl_inv:
assumes "cl_inv (g,p)"
shows "cl_inv (evalRecvArgs rargs xs g p)"
using assms
proof (induction rargs xs arbitrary: p g rule: list_induct2')
case (4 r rs x xs) thus ?case
proof (cases r)
case (RecvArgVar v)
with 4 have "cl_inv (setVar v x g p)"
by (auto intro!: setVar_cl_inv)
with "4.IH" RecvArgVar show ?thesis
by (auto split: prod.splits)
qed simp_all
qed simp_all
lemma evalEffect_pState_inv:
assumes "pState_inv prog p"
and "gState_inv prog g"
and "cl_inv (g,p)"
and "e ∈ effect ` edgeSet (states prog !! pState.idx p)"
shows "pState_inv prog (snd (evalEffect e prog g p))"
using assms
proof (cases e)
case (EEDecl d)
with assms have "d ∈ statesDecls (states prog !! pState.idx p)"
using statesDecls_effect
by simp
with assms EEDecl show ?thesis
by (auto simp del: IArray.sub_def
intro!: mkVarChannelProc_pState_inv)
next
case (EESend c es srt)
then obtain v where "ChanRef v = c" by (cases c) simp
with EESend assms show ?thesis
by (cases v) (auto simp add: withChannel'_def withVar'_def split: channel.split)
next
case (EERecv c es srt)
then obtain v where "ChanRef v = c" by (cases c) simp
with EERecv assms show ?thesis
by (cases v)
(auto simp: withChannel'_def withVar'_def
split: prod.splits channel.split
dest: evalRecvArgs_pState_inv')
qed (clarsimp_all intro!: setVar_pState_inv runProc_pState_inv)
lemma evalEffect_gState_progress_rel:
assumes "program_inv prog"
and "gState_inv prog g"
and "pState_inv prog p"
and "cl_inv (g,p)"
shows "(g, fst (evalEffect e prog g p)) ∈ gState_progress_rel prog"
using assms
proof (cases e)
case EEAssert
with assms show ?thesis
by (auto intro: setVar_gState_progress_rel)
next
case EEAssign
with assms show ?thesis
by (auto intro: setVar_gState_progress_rel)
next
case EEDecl
with assms show ?thesis
by (auto intro: mkVarChannelProc_gState_progress_rel)
next
case EERun
with assms show ?thesis
by (auto intro: runProc_gState_progress_rel)
next
case (EESend c es srt)
then obtain v where v: "c = ChanRef v" by (metis chanRef.exhaust)
obtain idx where idx: "nat_of_integer (the (getVar v g p)) = idx" by blast
note idx' = idx[symmetric, unfolded getVar_def]
show ?thesis
proof (cases "idx < length (gState.channels g)")
case True
note DEF = True EESend v idx' assms
show ?thesis
proof (cases "gState.channels g ! idx")
case (Channel cap ts q)
with True have "Channel cap ts q ∈ set (gState.channels g)"
by (metis nth_mem)
with assms have "channel_inv (Channel cap ts q)"
by (auto simp add: gState_inv_def simp del: channel_inv.simps)
with Channel DEF show ?thesis
by (cases v)
(auto simp add: withChannel'_def withVar'_def for_all_def
split: channel.split
intro!: gState_progress_rel_channels_update)
next
case HSChannel with DEF show ?thesis
by (cases v)
(auto simp: withChannel'_def withVar'_def gState_progress_rel_def
gState_inv_def
split: channel.split)
next
case InvChannel with DEF show ?thesis
by (cases v) (auto simp add: withChannel'_def withVar'_def)
qed
next
case False with EESend idx' v assms show ?thesis
by (cases v) (auto simp add: withChannel'_def withVar'_def)
qed
next
case (EERecv c rs srt rem)
then obtain v where v: "c = ChanRef v" by (metis chanRef.exhaust)
obtain idx where idx: "nat_of_integer (the (getVar v g p)) = idx" by blast
note idx' = idx[symmetric, unfolded getVar_def]
show ?thesis
proof (cases "idx < length (gState.channels g)")
case True
note DEF = True EERecv v idx' assms
show ?thesis
proof (cases "gState.channels g ! idx")
note channel_inv.simps[simp del]
case (Channel cap ts q)
with True have "Channel cap ts q ∈ set (gState.channels g)"
by (metis nth_mem)
with assms have c_inv: "channel_inv (Channel cap ts q)"
by (auto simp add: gState_inv_def simp del: channel_inv.simps)
moreover obtain res q' where
"apfst the (find_remove (recvArgsCheck g p rs) q) = (res, q')"
by (metis prod.exhaust)
moreover hence "q' = snd (find_remove (recvArgsCheck g p rs) q)"
by (simp add: apfst_def map_prod_def split: prod.splits)
with find_remove_subset find_remove_length have
"set q' ⊆ set q" "length q' ≤ length q"
by (metis surjective_pairing)+
with c_inv have "channel_inv (Channel cap ts q')"
by (auto simp add: channel_inv.simps)
moreover {
assume "q ≠ []"
hence "set (tl q) ⊆ set q" using tl_subset by auto
with c_inv have "channel_inv (Channel cap ts (tl q))"
by (auto simp add: channel_inv.simps)
}
moreover {
fix res g' p'
assume "evalRecvArgs rs res g p = (g',p')"
with evalRecvArgs_gState_progress_rel assms have
"(g,g') ∈ gState_progress_rel prog"
by (metis fst_conv)
hence "length (channels g) ≤ length (channels g')"
by (simp add: gState_progress_rel_def)
}
ultimately show ?thesis using Channel DEF
apply (cases v)
apply (auto simp add: withChannel'_def withVar'_def for_all_def
split: channel.split prod.split
elim: fstE
intro!: evalRecvArgs_gState_progress_rel
gState_progress_rel_channels_update_step)
apply force+
done
next
case HSChannel
obtain g' p' where *: "evalRecvArgs rs (hsdata g) g p = (g',p')"
by (metis prod.exhaust)
with assms have "(g,g') ∈ gState_progress_rel prog"
by (auto elim!: fstE intro!: evalRecvArgs_gState_progress_rel)
also hence "gState_inv prog g'" by blast
hence "(g',g'⦇handshake := 0, hsdata := []⦈) ∈ gState_progress_rel prog"
by (auto simp add: gState_progress_rel_def gState_inv_def)
finally
have "(g,g'⦇handshake := 0, hsdata := []⦈) ∈ gState_progress_rel prog" .
with DEF HSChannel * show ?thesis
by (cases v) (auto simp add: withChannel'_def withVar'_def for_all_def
split: channel.split prod.split)
next
case InvChannel with DEF show ?thesis
by (cases v) (auto simp add: withChannel'_def withVar'_def)
qed
next
case False with EERecv idx' v assms show ?thesis
by (cases v) (auto simp add: withChannel'_def withVar'_def)
qed
qed simp_all
lemma evalEffect_cl_inv:
assumes "cl_inv (g,p)"
and "program_inv prog"
and "gState_inv prog g"
and "pState_inv prog p"
shows "cl_inv (evalEffect e prog g p)"
using assms
proof (cases e)
case EERun with assms show ?thesis by (force intro!: runProc_cl_inv)
next
case (EESend c es srt) then obtain v where "ChanRef v = c" by (cases c) simp
with EESend assms show ?thesis
by (cases v)
(auto simp add: withChannel'_def withVar'_def split: channel.split
intro!: cl_inv_channels_update)
next
case (EERecv c es srt) then obtain v where "ChanRef v = c" by (cases c) simp
with EERecv assms show ?thesis
apply (cases v)
apply (auto simp add: withChannel'_def withVar'_def split: channel.split prod.split
intro!: cl_inv_channels_update)
apply (metis evalRecvArgs_cl_inv)+
done
qed (simp_all add: setVar_cl_inv mkVarChannelProc_cl_inv)
subsubsection ‹Executable edges›
text ‹
To find a successor global state, we first need to find all those edges which are executable
(\ie the condition evaluates to true).
›
type_synonym choices = "(edge * pState) list"
definition getChoices :: "gState⇩I ⇒ pState ⇒ edge list ⇒ choices" where
"getChoices g p = foldl (λE e.
if evalHandshake (cond e) (handshake g) g p ∧ evalCond (cond e) g p
then (e,p)#E
else E) []"
lemma getChoices_sub_edges_fst:
"fst ` set (getChoices g p es) ⊆ set es"
unfolding getChoices_def
by (rule foldl_rule_aux) auto
lemma getChoices_sub_edges:
"(a,b) ∈ set (getChoices g p es) ⟹ a ∈ set es"
using getChoices_sub_edges_fst
by force
lemma getChoices_p_snd:
"snd ` set (getChoices g p es) ⊆ {p}"
unfolding getChoices_def
by (rule foldl_rule_aux) auto
lemma getChoices_p:
"(a,b) ∈ set (getChoices g p es) ⟹ b = p"
using getChoices_p_snd
by force
definition sort_by_pri where
"sort_by_pri min_pri edges = foldl (λes e.
let idx = nat_of_integer (abs (prio e))
in if idx > min_pri
then abort STR ''Invalid priority'' (λ_. es)
else let ep = e # (es ! idx) in es[idx := ep]
) (replicate (min_pri + 1) []) edges"
lemma sort_by_pri_edges':
assumes "set edges ⊆ A"
shows "set (sort_by_pri min_pri edges) ⊆ {xs. set xs ⊆ A}"
using assms
unfolding sort_by_pri_def
apply (rule_tac I="λσ _. (∀x ∈ set σ. set x ⊆ A) ∧ length σ = min_pri + 1" in foldl_rule_aux_P)
apply simp
apply (force dest!: subsetD[OF set_update_subset_insert]
split: if_splits)
apply force
done
lemma sort_by_pri_edges:
assumes "set edges ⊆ A"
and "es ∈ set (sort_by_pri min_pri edges)"
shows "set es ⊆ A"
using sort_by_pri_edges'[OF assms(1)] assms
by auto
lemma sort_by_pri_length:
"length (sort_by_pri min_pri edges) = min_pri + 1"
unfolding sort_by_pri_def
by (rule foldl_rule_aux_P [where I="λσ _. length σ = min_pri + 1"])
simp_all
definition executable
:: "states iarray ⇒ gState⇩I ⇒ choices nres"
where
"executable ss g = (
let procs = procs g in
nfoldli procs (λ_. True) (λp E.
if (exclusive g = 0 ∨ exclusive g = pid p) then do {
let (min_pri, edges) = (ss !! pState.idx p) !! pc p;
ASSERT(set edges ⊆ edgeSet (ss !! pState.idx p));
(E',_,_) ←
if min_pri = 0 then do {
WHILE⇩T (λ(E,brk,_). E = [] ∧ brk = 0) (λ (_, _, ELSE). do {
let g = g⦇gState⇩I.else := ELSE⦈;
E = getChoices g p edges
in
if E = [] then (
if ¬ ELSE then RETURN (E, 0::nat, True)
else RETURN (E, 1, False))
else RETURN (E, 1, ELSE) }) ([], 0::nat, False)
} else do {
let min_pri = nat_of_integer (abs min_pri);
let pri_edges = sort_by_pri min_pri edges;
ASSERT (∀es ∈ set pri_edges.
set es ⊆ edgeSet (ss !! pState.idx p));
let pri_edges = IArray pri_edges;
WHILE⇩T (λ(E,pri,_). E = [] ∧ pri ≤ min_pri) (λ(_, pri, ELSE). do {
let es = pri_edges !! pri;
let g = g⦇gState⇩I.else := ELSE⦈;
let E = getChoices g p es;
if E = [] then (
if ¬ ELSE then RETURN (E,pri,True)
else RETURN (E, pri + 1, False))
else RETURN (E, pri, ELSE) }) ([], 0, False)
};
RETURN (E'@E)
} else RETURN E
) []
)"
definition
"while_rel1 =
measure (λx. if x = [] then 1 else 0)
<*lex*> measure (λx. if x = 0 then 1 else 0)
<*lex*> measure (λx. if ¬ x then 1 else 0)"
lemma wf_while_rel1:
"wf while_rel1"
unfolding while_rel1_def
by auto
definition
"while_rel2 mp =
measure (λx. if x = [] then 1 else 0)
<*lex*> measure (λx. (mp + 1) - x)
<*lex*> measure (λx. if ¬ x then 1 else 0)"
lemma wf_while_rel2:
"wf (while_rel2 mp)"
unfolding while_rel2_def
by auto
lemma executable_edgeSet:
assumes "gState_inv prog g"
and "program_inv prog"
and "ss = states prog"
shows "executable ss g
≤ SPEC (λcs. ∀(e,p) ∈ set cs.
e ∈ edgeSet (ss !! pState.idx p)
∧ pState_inv prog p
∧ cl_inv (g,p))"
unfolding executable_def
using assms
apply (refine_rcg refine_vcg nfoldli_rule[where
I="λ_ _ cs. ∀(e,p) ∈ set cs.
e ∈ edgeSet (ss !! pState.idx p)
∧ pState_inv prog p
∧ cl_inv (g,p)"])
apply simp
apply (rename_tac p l1 l2 σ e p')
apply (subgoal_tac "pState_inv prog p")
apply (clarsimp simp add: edgeSet_def pState_inv_def)[]
apply (rule_tac x="IArray.list_of
(IArray.list_of (states prog) ! pState.idx p) ! pc p" in bexI)
apply simp
apply (force intro!: nth_mem)
apply (force simp add: gState_inv_def)
apply (refine_rcg refine_vcg wf_while_rel1 WHILET_rule[where
I="λ(cs,_,_). ∀(e,p) ∈ set cs.
e ∈ edgeSet (ss !! pState.idx p)
∧ pState_inv prog p
∧ cl_inv (g,p)"
and R=while_rel1])
apply (vc_solve solve: asm_rl simp add: while_rel1_def)
apply (frule getChoices_p)
using getChoices_sub_edges apply (force simp add: gState_inv_def)
using sort_by_pri_edges apply fastforce
apply (rename_tac min_pri pri_edges)
apply (rule_tac I="λ(cs,_,_). ∀(e,p) ∈ set cs.
e ∈ edgeSet (ss !! pState.idx p)
∧ pState_inv prog p
∧ cl_inv (g,p)"
and R="while_rel2 (nat_of_integer (abs min_pri))"
in WHILET_rule)
apply (simp add: wf_while_rel2)
apply simp
apply (refine_rcg refine_vcg)
apply (clarsimp_all split: prod.split simp add: while_rel2_def)
apply (metis diff_less_mono lessI)
apply (rename_tac idx' else e p')
apply (frule getChoices_p)
apply (frule getChoices_sub_edges)
apply (subgoal_tac
"sort_by_pri (nat_of_integer ¦min_pri¦) pri_edges ! idx'
∈ set (sort_by_pri (nat_of_integer ¦min_pri¦) pri_edges)")
apply (auto simp add: assms gState_inv_def)[]
apply (force simp add: sort_by_pri_length)
apply (auto simp add: assms)
done
lemma executable_edgeSet':
assumes "gState_inv prog g"
and "program_inv prog"
shows "executable (states prog) g
≤ SPEC (λcs. ∀(e,p) ∈ set cs.
e ∈ edgeSet ((states prog) !! pState.idx p)
∧ pState_inv prog p
∧ cl_inv(g,p))"
using executable_edgeSet[where ss = "states prog"] assms
by simp
schematic_goal executable_refine:
"RETURN (?ex s g) ≤ executable s g"
unfolding executable_def
by (refine_transfer)
concrete_definition executable_impl for s g uses executable_refine
subsubsection ‹Successor calculation›
function to⇩I where
"to⇩I ⦇ gState.vars = v, channels = ch, timeout = t, procs = p ⦈
= ⦇ gState.vars = v, channels = ch, timeout = False, procs = p,
handshake = 0, hsdata = [], exclusive = 0, gState⇩I.else = False ⦈"
by (metis gState.cases) (metis gState.ext_inject)
termination by lexicographic_order
function "from⇩I" where
"from⇩I ⦇ gState.vars = v, channels = ch, timeout = t, procs = p, … = m ⦈
= ⦇ gState.vars = v, channels = ch, timeout = t, procs = p ⦈"
by (metis gState.surjective) (metis gState.ext_inject)
termination by lexicographic_order
function reset⇩I where
"reset⇩I ⦇ gState.vars = v, channels = ch, timeout = t, procs = p,
handshake = hs, hsdata = hsd, exclusive = _, gState⇩I.else = _ ⦈
= ⦇ gState.vars = v, channels = ch, timeout = False, procs = p,
handshake = 0, hsdata = if hs ≠ 0 then hsd else [], exclusive = 0,
gState⇩I.else = False ⦈"
by (metis (full_types) gState⇩I.surjective unit.exhaust)
(metis gState.select_convs gState⇩I.select_convs)
termination by lexicographic_order
lemma gState_inv_to⇩I:
"gState_inv prog g = gState_inv prog (to⇩I g)"
by (cases g, simp add: gState_inv_def cl_inv_def)
lemma gState_inv_from⇩I:
"gState_inv prog g = gState_inv prog (from⇩I g)"
by (cases g, simp add: gState_inv_def cl_inv_def)
lemma gState_inv_reset⇩I:
"gState_inv prog g = gState_inv prog (reset⇩I g)"
by (cases g, simp add: gState_inv_def cl_inv_def)
lemmas gState_inv_I_simps =
gState_inv_to⇩I gState_inv_from⇩I gState_inv_reset⇩I
definition removeProcs
where
"removeProcs ps = foldr (λp (dead,sd,ps,dcs).
if dead ∧ pc p = 0 then (True, True, ps, pState.channels p @ dcs)
else (False, sd, p#ps, dcs)) ps (True, False, [], [])"
lemma removeProcs_subset':
"set (fst (snd (snd (removeProcs ps)))) ⊆ set ps"
unfolding removeProcs_def
apply (subst foldr_conv_foldl)
apply (rule foldl_rule_aux_P[where I="λ(_,_,ps',_) _. set ps' ⊆ set ps"])
apply simp
apply (clarsimp split: if_splits)
apply force
apply (rename_tac p)
apply (case_tac "p = x")
apply (subst set_rev[symmetric])
apply simp
apply force
apply force
done
lemma removeProcs_length':
"length (fst (snd (snd (removeProcs ps)))) ≤ length ps"
unfolding removeProcs_def
apply (subst foldr_conv_foldl)
apply (rule foldl_rule_aux_P[where
I="λ(_,_,ps',_) ps''. length ps' + length ps'' ≤ length ps"])
apply (auto split: if_splits)
done
lemma removeProcs_subset:
"removeProcs ps = (dead,sd,ps',dcs) ⟹ set ps' ⊆ set ps"
using removeProcs_subset'
by (metis fst_conv snd_conv)
lemma removeProcs_length:
"removeProcs ps = (dead,sd,ps',dcs) ⟹ length ps' ≤ length ps"
using removeProcs_length'
by (metis fst_conv snd_conv)
definition cleanChans :: "integer list ⇒ channels ⇒ channels"
where
"cleanChans dchans cs = snd (foldl (λ(i,cs) c.
if List.member dchans i then (i + 1, cs@[InvChannel])
else (i + 1, cs@[c])) (0, []) cs)"
lemma cleanChans_channel_inv:
assumes "set cs ⊆ Collect channel_inv"
shows "set (cleanChans dchans cs) ⊆ Collect channel_inv"
using assms
unfolding cleanChans_def
apply (rule_tac foldl_rule_aux)
apply (force split: if_splits)+
done
lemma cleanChans_length:
"length (cleanChans dchans cs) = length cs"
unfolding cleanChans_def
by (rule foldl_rule_aux_P[where
I="λ(_,cs') cs''. length cs' + length cs'' = length cs"])
(force split: if_splits)+
definition checkDeadProcs :: "'a gState_scheme ⇒ 'a gState_scheme" where
"checkDeadProcs g = (
let (_, soDied, procs, dchans) = removeProcs (procs g) in
if soDied then
g⦇ procs := procs, channels := cleanChans dchans (channels g)⦈
else g)"
lemma checkDeadProcs_gState_progress_rel:
assumes "gState_inv prog g"
shows "(g, checkDeadProcs g) ∈ gState_progress_rel prog"
using assms cleanChans_length[where cs="channels g"]
cleanChans_channel_inv[where cs="channels g"]
unfolding checkDeadProcs_def
apply (intro gState_progress_relI)
apply assumption
apply (clarsimp split: if_splits prod.splits)
apply (frule removeProcs_length)
apply (frule removeProcs_subset)
apply (auto simp add: gState_inv_def cl_inv_def)[]
apply (clarsimp split: if_splits prod.splits)+
done
lemma gState_progress_rel_exclusive:
"(g, g') ∈ gState_progress_rel prog
⟹ (g, g'⦇exclusive := p⦈) ∈ gState_progress_rel prog"
by (simp add: gState_progress_rel_def gState_inv_def cl_inv_def)
definition applyEdge
:: "program ⇒ edge ⇒ pState ⇒ gState⇩I ⇒ gState⇩I nres"
where
"applyEdge prog e p g = do {
let (g',p') = evalEffect (effect e) prog g p;
ASSERT ((g,g') ∈ gState_progress_rel prog);
ASSERT (pState_inv prog p');
ASSERT (cl_inv (g',p'));
let p'' = (case target e of Index t ⇒
if t < IArray.length (states prog !! pState.idx p') then p'⦇pc := t⦈
else abort STR ''Edge target out of bounds'' (λ_. p')
| _ ⇒ abort STR ''Edge target not Index'' (λ_. p'));
ASSERT (pState_inv prog p'');
let g'' = g'⦇procs := list_update (procs g') (pid p'' - 1) p''⦈;
ASSERT ((g',g'') ∈ gState_progress_rel prog);
let g''' = (if isAtomic e ∧ handshake g'' = 0
then g''⦇ exclusive := pid p'' ⦈
else g'');
ASSERT ((g',g''') ∈ gState_progress_rel prog);
let g⇩f = (if pc p'' = 0 then checkDeadProcs g''' else g''');
ASSERT ((g''',g⇩f) ∈ gState_progress_rel prog);
RETURN g⇩f }"
lemma applyEdge_gState_progress_rel:
assumes "program_inv prog"
and "gState_inv prog g"
and "pState_inv prog p"
and "cl_inv (g,p)"
and "e ∈ edgeSet (states prog !! pState.idx p)"
shows "applyEdge prog e p g ≤ SPEC (λg'. (g,g') ∈ gState_progress_rel prog)"
using assms
unfolding applyEdge_def
apply (intro refine_vcg)
apply (force elim: fstE intro!: evalEffect_gState_progress_rel)
apply (force elim: sndE intro!: evalEffect_pState_inv)
apply (drule subst)
apply (rule evalEffect_cl_inv)
apply assumption+
apply (cases "target e")
apply (clarsimp simp add: pState_inv_def)
apply simp
apply (frule gState_progress_rel_gState_invI2)
apply (cases "target e")
apply (clarsimp split: if_splits)
apply (intro gState_progress_relI)
apply assumption
apply (auto simp add: gState_inv_def cl_inv_def
dest!: subsetD[OF set_update_subset_insert])[]
apply (simp add: cl_inv_def)
apply simp
apply (intro gState_progress_relI)
apply assumption
apply (auto simp add: gState_inv_def cl_inv_def
dest!: subsetD[OF set_update_subset_insert])[]
apply (simp add: cl_inv_def)
apply simp
apply (clarsimp split: if_splits)
apply (intro gState_progress_relI)
apply assumption
apply (auto simp add: gState_inv_def cl_inv_def
dest!: subsetD[OF set_update_subset_insert])[]
apply (simp add: cl_inv_def)
apply simp
apply (auto split: if_splits intro!: gState_progress_rel_exclusive)[]
apply (force intro!: checkDeadProcs_gState_progress_rel)
apply (blast intro!: gState_progress_rel_trans)
done
schematic_goal applyEdge_refine:
"RETURN (?ae prog e p g) ≤ applyEdge prog e p g"
unfolding applyEdge_def
by (refine_transfer)
concrete_definition applyEdge_impl for e p g uses applyEdge_refine
definition nexts
:: "program ⇒ gState ⇒ gState ls nres"
where
"nexts prog g = (
let
f = from⇩I;
g = to⇩I g
in
REC (λD g. do {
E ← executable (states prog) g;
if E = [] then
if handshake g ≠ 0 then
RETURN (ls.empty())
else if exclusive g ≠ 0 then
RETURN (ls.sng (f g))
else if ¬ timeout g then
D (g⦇timeout := True⦈)
else
RETURN (ls.sng (f (reset⇩I g)))
else
let g = reset⇩I g in
nfoldli E (λ_. True) (λ(e,p) G.
applyEdge prog e p g ⤜ (λ g'.
if handshake g' ≠ 0 ∨ isAtomic e then do {
G⇩R ← D g';
if ls.isEmpty G⇩R ∧ handshake g' = 0 then
RETURN (ls.ins (f g') G)
else
RETURN (ls.union G⇩R G)
} else RETURN (ls.ins (f g') G))) (ls.empty())
}) g
⤜ (λG. if ls.isEmpty G then RETURN (ls.sng (f g)) else RETURN G)
)"
lemma gState_progress_rel_intros:
"(to⇩I g, gI') ∈ gState_progress_rel prog
⟹ (g, from⇩I gI') ∈ gState_progress_rel prog"
"(gI, gI') ∈ gState_progress_rel prog
⟹ (gI, reset⇩I gI') ∈ gState_progress_rel prog"
"(to⇩I g, gI') ∈ gState_progress_rel prog
⟹ (to⇩I g, gI'⦇timeout := t⦈) ∈ gState_progress_rel prog"
unfolding gState_progress_rel_def
by (cases g, cases gI', cases gI, force simp add: gState_inv_def cl_inv_def)+
lemma gState_progress_rel_step_intros:
"(to⇩I g, g') ∈ gState_progress_rel prog
⟹ (reset⇩I g', g'') ∈ gState_progress_rel prog
⟹ (g, from⇩I g'') ∈ gState_progress_rel prog"
"(to⇩I g, g') ∈ gState_progress_rel prog
⟹ (reset⇩I g', g'') ∈ gState_progress_rel prog
⟹ (to⇩I g, g'') ∈ gState_progress_rel prog"
unfolding gState_progress_rel_def
by (cases g, cases g', cases g'', force simp add: gState_inv_def cl_inv_def)+
lemma cl_inv_reset⇩I:
"cl_inv(g,p) ⟹ cl_inv(reset⇩I g, p)"
by (cases g) (simp add: cl_inv_def)
lemmas refine_helpers =
gState_progress_rel_intros gState_progress_rel_step_intros cl_inv_reset⇩I
lemma nexts_SPEC:
assumes "gState_inv prog g"
and "program_inv prog"
shows "nexts prog g ≤ SPEC (λgs. ∀g' ∈ ls.α gs. (g,g') ∈ gState_progress_rel prog)"
using assms
unfolding nexts_def
apply (refine_rcg refine_vcg REC_rule[where
pre="λg'. (to⇩I g,g') ∈ gState_progress_rel prog"])
apply (simp add: gState_inv_to⇩I)
apply (rule order_trans[OF executable_edgeSet'])
apply (drule gState_progress_rel_gState_invI2)
apply assumption
apply assumption
apply (refine_rcg refine_vcg nfoldli_rule[where
I="λ_ _ σ. ∀g' ∈ ls.α σ. (g,g') ∈ gState_progress_rel prog"]
order_trans[OF applyEdge_gState_progress_rel])
apply (vc_solve intro: refine_helpers solve: asm_rl simp add: ls.correct)
apply (rule order_trans)
apply (rprems)
apply (vc_solve intro: refine_helpers solve: asm_rl simp add: ls.correct)
apply (rule order_trans)
apply rprems
apply (vc_solve intro: refine_helpers solve: asm_rl simp add: ls.correct)
done
lemma RETURN_dRETURN:
"RETURN f ≤ f' ⟹ nres_of (dRETURN f) ≤ f'"
unfolding nres_of_def
by simp
lemma executable_dRETURN:
"nres_of (dRETURN (executable_impl prog g)) ≤ executable prog g"
using executable_impl.refine
by (simp add: RETURN_dRETURN)
lemma applyEdge_dRETURN:
"nres_of (dRETURN (applyEdge_impl prog e p g)) ≤ applyEdge prog e p g"
using applyEdge_impl.refine
by (simp add: RETURN_dRETURN)
schematic_goal nexts_code_aux:
"nres_of (?nexts prog g) ≤ nexts prog g"
unfolding nexts_def
by (refine_transfer the_resI executable_dRETURN applyEdge_dRETURN)
concrete_definition nexts_code_aux for prog g uses nexts_code_aux
prepare_code_thms nexts_code_aux_def
subsubsection ‹Handle non-termination›
text ‹
A Promela model may include non-terminating parts. Therefore we cannot guarantee, that @{const nexts} will actually terminate.
To avoid having to deal with this in the model checker, we fail in case of non-termination.
›
definition SUCCEED_abort where
"SUCCEED_abort msg dm m = (
case m of
RES X ⇒ if X={} then Code.abort msg (λ_. dm) else RES X
| _ ⇒ m)"
definition dSUCCEED_abort where
"dSUCCEED_abort msg dm m = (
case m of
dSUCCEEDi ⇒ Code.abort msg (λ_. dm)
| _ ⇒ m)"
definition ref_succeed where
"ref_succeed m m' ⟷ m ≤ m' ∧ (m=SUCCEED ⟶ m'=SUCCEED)"
lemma dSUCCEED_abort_SUCCEED_abort:
"⟦ RETURN dm' ≤ dm; ref_succeed (nres_of m') m ⟧
⟹ nres_of (dSUCCEED_abort msg (dRETURN dm') (m'))
≤ SUCCEED_abort msg dm m"
unfolding dSUCCEED_abort_def SUCCEED_abort_def ref_succeed_def
by (auto split: dres.splits nres.splits)
text ‹The final successor function now incorporates:
\begin{enumerate}
\item @{const Promela.nexts}
\item handling of non-termination
\end{enumerate}›
definition nexts_code where
"nexts_code prog g =
the_res (dSUCCEED_abort (STR ''The Universe is broken!'')
(dRETURN (ls.sng g))
(nexts_code_aux prog g))"
lemma nexts_code_SPEC:
assumes "gState_inv prog g"
and "program_inv prog"
shows "g' ∈ ls.α (nexts_code prog g)
⟹ (g,g') ∈ gState_progress_rel prog"
unfolding nexts_code_def
unfolding dSUCCEED_abort_def
using assms
using order_trans[OF nexts_code_aux.refine nexts_SPEC[OF assms(1,2)]]
by (auto split: dres.splits simp: ls.correct)
subsection ‹Finiteness of the state space›
inductive_set reachable_states
for P :: program
and g⇩s :: gState
where
"g⇩s ∈ reachable_states P g⇩s" |
"g ∈ reachable_states P g⇩s ⟹ x ∈ ls.α (nexts_code P g)
⟹ x ∈ reachable_states P g⇩s"
lemmas reachable_states_induct[case_names init step] =
reachable_states.induct[split_format (complete)]
lemma reachable_states_finite:
assumes "program_inv prog"
and "gState_inv prog g"
shows "finite (reachable_states prog g)"
proof (rule finite_subset[OF _ gStates_finite[of _ g]])
define INV where "INV g' ⟷ g' ∈ (gState_progress_rel prog)⇧* `` {g} ∧ gState_inv prog g'" for g'
{
fix g'
have "g' ∈ reachable_states prog g ⟹ INV g'"
proof (induct rule: reachable_states_induct)
case init with assms show ?case by (simp add: INV_def)
next
case (step g g')
from step(2,3) have
"(g, g') ∈ gState_progress_rel prog"
using nexts_code_SPEC[OF _ ‹program_inv prog›]
unfolding INV_def by auto
thus ?case using step(2) unfolding INV_def by auto
qed
}
thus "reachable_states prog g ⊆
(gState_progress_rel prog)⇧* `` {g}"
unfolding INV_def by auto
qed
subsection ‹Traces›
text ‹When trying to generate a lasso, we have a problem: We only have a list of global
states. But what are the transitions to come from one to the other?
This problem shall be tackled by @{term replay}: Given two states, it generates a list of
transitions that was taken.›
definition replay :: "program ⇒ gState ⇒ gState ⇒ choices nres" where
"replay prog g⇩1 g⇩2 = (
let
g⇩1 = to⇩I g⇩1;
check = λg. from⇩I g = g⇩2
in
REC⇩T (λD g. do {
E ← executable (states prog) g;
if E = [] then
if check g then RETURN []
else if ¬ timeout g then D (g⦇timeout := True⦈)
else abort STR ''Stuttering should not occur on replay''
(λ_. RETURN [])
else
let g = reset⇩I g in
nfoldli E (λE. E = []) (λ(e,p) _.
applyEdge prog e p g ⤜ (λg'.
if handshake g' ≠ 0 ∨ isAtomic e then do {
E⇩R ← D g';
if E⇩R = [] then
if check g' then RETURN [(e,p)] else RETURN []
else
RETURN ((e,p) # E⇩R)
} else if check g' then RETURN [(e,p)] else RETURN [])
) []
}) g⇩1
)"
lemma abort_refine[refine_transfer]:
"nres_of (f ()) ≤ F () ⟹ nres_of (abort s f) ≤ abort s F"
"f() ≠ dSUCCEED ⟹ abort s f ≠ dSUCCEED"
by auto
schematic_goal replay_code_aux:
"RETURN (?replay prog g⇩1 g⇩2) ≤ replay prog g⇩1 g⇩2"
unfolding replay_def applyEdge_def
by (refine_transfer the_resI executable_dRETURN)
concrete_definition replay_code for prog g⇩1 g⇩2 uses replay_code_aux
prepare_code_thms replay_code_def
subsubsection ‹Printing of traces›
definition procDescr
:: "(integer ⇒ string) ⇒ program ⇒ pState ⇒ string"
where
"procDescr f prog p = (
let
name = String.explode (proc_names prog !! pState.idx p);
id = f (integer_of_nat (pid p))
in
name @ '' ('' @ id @ '')'')"
definition printInitial
:: "(integer ⇒ string) ⇒ program ⇒ gState ⇒ string"
where
"printInitial f prog g⇩0 = (
let psS = printList (procDescr f prog) (procs g⇩0) [] [] '' '' in
''Initially running: '' @ psS)"
abbreviation "lf ≡ CHR 0x0A"
fun printConfig
:: "(integer ⇒ string) ⇒ program ⇒ gState option ⇒ gState ⇒ string"
where
"printConfig f prog None g⇩0 = printInitial f prog g⇩0"
| "printConfig f prog (Some g⇩0) g⇩1 = (
let eps = replay_code prog g⇩0 g⇩1 in
let print = (λ(e,p). procDescr f prog p @ '': '' @ printEdge f (pc p) e)
in if eps = [] ∧ g⇩1 = g⇩0 then '' -- stutter --''
else printList print eps [] [] (lf#'' ''))"
definition "printConfigFromAST f ≡ printConfig f o fst o setUp"
subsection ‹Code export›
code_identifier
code_module "PromelaInvariants" ⇀ (SML) Promela
| code_module "PromelaDatastructures" ⇀ (SML) Promela
definition "executable_triv prog g = executable_impl (snd prog) g"
definition "apply_triv prog g ep = applyEdge_impl prog (fst ep) (snd ep) (reset⇩I g)"
export_code
setUp printProcesses printConfigFromAST nexts_code executable_triv apply_triv
extractLTLs lookupLTL
checking SML
export_code
setUp printProcesses printConfigFromAST nexts_code executable_triv apply_triv
extractLTLs lookupLTL
in SML
file ‹Promela.sml›
end