header {* \isaheader{State Space Exploration} *}
theory Exploration
imports Main "../common/Misc" "../DatRef"
begin
text_raw {*\label{thy:Exploration}*}
text {*
In this theory, a workset algorithm for state-space exploration is defined.
It explores the set of states that are reachable by a given relation,
starting at a given set of initial states.
The specification makes use of the data refinement framework for
while-algorithms (cf. Section~\ref{thy:DatRef}), and is thus suited for
being refined to an executable algorithm, using the Isabelle Collections Framework
to provide the necessary data structures.
*}
subsection "Generic Search Algorithm"
-- "The algorithm contains a set of discovered states and a workset"
type_synonym 'Σ sse_state = "'Σ set × 'Σ set"
-- "Loop body"
inductive_set
sse_step :: "('Σ×'Σ) set => ('Σ sse_state × 'Σ sse_state) set"
for R where
"[| σ∈W;
Σ' = Σ ∪ (R``{σ});
W' = (W-{σ}) ∪ ((R``{σ}) - Σ)
|] ==> ((Σ,W),(Σ',W'))∈sse_step R"
-- "Loop condition"
definition sse_cond :: "'Σ sse_state set" where
"sse_cond = {(Σ,W). W≠{}}"
-- "Initial state"
definition sse_initial :: "'Σ set => 'Σ sse_state" where
"sse_initial Σi == (Σi,Σi)"
-- {*Invariants:
\begin{itemize}
\item The workset contains only states that are already
discovered.
\item All discovered states are target states
\item If there is a target state that is not discovered yet,
then there is an element in the workset from that this
target state is reachable without using discovered
states as intermediate states. This supports the intuition
of the workset as a frontier between the sets of discovered
and undiscovered states.
\end{itemize}*}
definition sse_invar :: "'Σ set => ('Σ×'Σ) set => 'Σ sse_state set" where
"sse_invar Σi R = {(Σ,W).
W⊆Σ ∧
(Σ ⊆ R⇧*``Σi) ∧
(∀σ∈(R⇧*``Σi)-Σ. ∃σh∈W. (σh,σ)∈(R - (UNIV × Σ))⇧*)
}"
definition "sse_algo Σi R ==
(| wa_cond=sse_cond,
wa_step=sse_step R,
wa_initial = {sse_initial Σi},
wa_invar = sse_invar Σi R |)),"
definition "sse_term_rel Σi R ==
{ (σ',σ). σ∈sse_invar Σi R ∧ (σ,σ')∈sse_step R }"
-- "Termination: Either a new state is discovered, or the workset shrinks"
theorem sse_term:
assumes finite[simp, intro!]: "finite (R⇧*``Σi)"
shows "wf (sse_term_rel Σi R)"
proof -
have "wf (({(Σ',Σ). Σ ⊂ Σ' ∧ Σ' ⊆ (R⇧*``Σi)}) <*lex*> finite_psubset)"
by (auto intro: wf_bounded_supset)
moreover have "sse_term_rel Σi R ⊆ …" (is "_ ⊆ ?R")
proof
fix S
assume A: "S∈sse_term_rel Σi R"
obtain Σ W Σ' W' σ where
[simp]: "S=((Σ',W'),(Σ,W))" and
S: "(Σ,W) ∈ sse_invar Σi R"
"σ∈W"
"Σ' = Σ ∪ R``{σ}"
"W' = (W-{σ}) ∪ (R``{σ} - Σ)"
proof -
obtain Σ W Σ' W' where SF[simp]: "S=((Σ',W'),(Σ,W))" by (cases S) force
from A have R: "(Σ,W) ∈ sse_invar Σi R" "((Σ,W),(Σ',W'))∈sse_step R"
by (auto simp add: sse_term_rel_def)
from sse_step.cases[OF R(2)] obtain σ where S:
"σ∈W"
"Σ' = Σ ∪ R``{σ}"
"W' = (W-{σ}) ∪ (R``{σ} - Σ)"
by metis
thus ?thesis
by (rule_tac that[OF SF R(1) S])
qed
from S(1) have
[simp, intro!]: "finite Σ" "finite W" and
WSS: "W⊆Σ" and
SSS: "Σ⊆R⇧*``Σi"
by (auto simp add: sse_invar_def intro: finite_subset)
show "S∈?R" proof (cases "R``{σ} ⊆ Σ")
case True with S have "Σ'=Σ" "W' ⊂ W" by auto
thus ?thesis by (simp)
next
case False
with S have "Σ' ⊃ Σ" by auto
moreover from S(2) WSS SSS have "σ∈R⇧*``Σi" by auto
hence "R``{σ} ⊆ R⇧*``Σi"
by (auto intro: rtrancl_into_rtrancl)
with S(3) SSS have "Σ' ⊆ R⇧*``Σi" by auto
ultimately show ?thesis by simp
qed
qed
ultimately show ?thesis by (auto intro: wf_subset)
qed
lemma sse_invar_initial: "(sse_initial Σi) ∈ sse_invar Σi R"
by (unfold sse_invar_def sse_initial_def)
(auto elim: rtrancl_last_touch)
-- "Correctness theorem: If the loop terminates, the discovered states are
exactly the reachable states"
theorem sse_invar_final:
"∀S. S∈wa_invar (sse_algo Σi R) ∧ S∉wa_cond (sse_algo Σi R)
--> fst S = R⇧*``Σi"
by (intro allI, case_tac S)
(auto simp add: sse_invar_def sse_cond_def sse_algo_def)
lemma sse_invar_step: "[|S∈sse_invar Σi R; (S,S')∈sse_step R|]
==> S'∈sse_invar Σi R"
-- "Split the goal by the invariant:"
apply (cases S, cases S')
apply clarsimp
apply (erule sse_step.cases)
apply clarsimp
apply (subst sse_invar_def)
apply (simp add: Let_def split_conv)
apply (intro conjI)
-- "Solve the easy parts automatically"
apply (auto simp add: sse_invar_def) [3]
apply (force simp add: sse_invar_def
dest: rtrancl_into_rtrancl) [1]
-- "Tackle the complex part (last part of the invariant) in Isar"
proof (intro ballI)
fix σ W Σ σ'
assume A:
"(Σ,W)∈sse_invar Σi R"
"σ∈W"
"σ'∈R⇧* `` Σi - (Σ ∪ R `` {σ})"
-- "Using the invariant of the original state, we obtain
a state in the original workset and a path not touching
the originally discovered states"
from A(3) have "σ' ∈ R⇧* `` Σi - Σ" by auto
with A(1) obtain σh where IP:
"σh∈W"
"(σh,σ')∈(R - (UNIV × Σ))⇧*"
and SS:
"W⊆Σ"
"Σ⊆R⇧* `` Σi"
by (unfold sse_invar_def) force
-- {* We now make a case distinction, whether the obtained path contains
states from @{term "post σ"} or not: *}
from IP(2) show "∃σh∈W - {σ} ∪ (R `` {σ} - Σ).
(σh, σ') ∈ (R - UNIV × (Σ ∪ R `` {σ}))⇧*"
proof (cases rule: rtrancl_last_visit[where S="R `` {σ}"])
case no_visit
-- {* In the case that the obtained path contains no states from
@{term "post σ"}, we can take it. *}
hence G1: "(σh,σ')∈(R- (UNIV × (Σ∪R `` {σ})))⇧*"
by (simp add: set_diff_diff_left Sigma_Un_distrib2)
moreover have "σh ≠ σ"
-- {* We may exclude the case that our obtained path started at
@{text σ}, as all successors of @{text σ} are
in @{term "R `` {σ}"} *}
proof
assume [simp]: "σh=σ"
from A SS have "σ≠σ'" by auto
with G1 show False
by (auto simp add: elim: converse_rtranclE)
qed
ultimately show ?thesis using IP(1) by auto
next
case (last_visit_point σt)
-- {* If the obtained path contains a state from @{text "R `` {σ}"},
we simply pick the last one: *}
hence "(σt,σ')∈(R- (UNIV × (Σ∪R `` {σ})))⇧*"
by (simp add: set_diff_diff_left Sigma_Un_distrib2)
moreover from last_visit_point(2) have "σt∉Σ"
by (auto elim: trancl.cases)
ultimately show ?thesis using last_visit_point(1) by auto
qed
qed
-- "The sse-algorithm is a well-defined while-algorithm"
theorem sse_while_algo: "finite (R⇧*``Σi) ==> while_algo (sse_algo Σi R)"
apply unfold_locales
apply (auto simp add: sse_algo_def intro: sse_invar_step sse_invar_initial)
apply (drule sse_term)
apply (erule_tac wf_subset)
apply (unfold sse_term_rel_def)
apply auto
done
subsection "Depth First Search"
text_raw {*\label{sec:sse:dfs}*}
text {*
In this section, the generic state space exploration algorithm is refined
to a DFS-algorithm, that uses a stack to implement the workset.
*}
type_synonym 'Σ dfs_state = "'Σ set × 'Σ list"
definition dfs_α :: "'Σ dfs_state => 'Σ sse_state"
where "dfs_α S == let (Σ,W)=S in (Σ,set W)"
definition dfs_invar_add :: "'Σ dfs_state set"
where "dfs_invar_add == {(Σ,W). distinct W}"
definition "dfs_invar Σi R == dfs_invar_add ∩ { s. dfs_α s ∈ sse_invar Σi R }"
inductive_set dfs_initial :: "'Σ set => 'Σ dfs_state set" for Σi
where "[| distinct W; set W = Σi|] ==> (Σi,W)∈dfs_initial Σi"
inductive_set dfs_step :: "('Σ×'Σ) set => ('Σ dfs_state ×'Σ dfs_state) set"
for R where
"[| W=σ#Wtl;
distinct Wn;
set Wn = R``{σ} - Σ;
W' = Wn@Wtl;
Σ' = R``{σ} ∪ Σ
|] ==> ((Σ,W),(Σ',W'))∈dfs_step R"
definition dfs_cond :: "'Σ dfs_state set"
where "dfs_cond == { (Σ,W). W≠[]}"
definition "dfs_algo Σi R == (|
wa_cond = dfs_cond,
wa_step = dfs_step R,
wa_initial = dfs_initial Σi,
wa_invar = dfs_invar Σi R |)),"
-- "The DFS-algorithm refines the state-space exploration algorithm"
theorem dfs_pref_sse:
"wa_precise_refine (dfs_algo Σi R) (sse_algo Σi R) dfs_α"
apply (unfold_locales)
apply (auto simp add: dfs_algo_def sse_algo_def dfs_cond_def sse_cond_def
dfs_α_def)
apply (erule dfs_step.cases)
apply (rule_tac σ=σ in sse_step.intros)
apply (auto simp add: dfs_invar_def sse_invar_def dfs_invar_add_def
sse_initial_def dfs_α_def
elim: dfs_initial.cases)
done
-- "The DFS-algorithm is a well-defined while-algorithm"
theorem dfs_while_algo:
assumes finite[simp, intro!]: "finite (R⇧*``Σi)"
shows "while_algo (dfs_algo Σi R)"
proof -
interpret wa_precise_refine "(dfs_algo Σi R)" "(sse_algo Σi R)" dfs_α
using dfs_pref_sse .
have [simp]: "wa_invar (sse_algo Σi R) = sse_invar Σi R"
by (simp add: sse_algo_def)
show ?thesis
apply (rule wa_intro)
apply (simp add: sse_while_algo)
apply (simp add: dfs_invar_def dfs_algo_def)
apply (auto simp add: dfs_invar_add_def dfs_algo_def dfs_α_def
dfs_cond_def sse_invar_def
elim!: dfs_step.cases) [1]
apply (auto simp add: dfs_invar_add_def dfs_algo_def
elim: dfs_initial.cases) [1]
done
qed
-- "The result of the DFS-algorithm is correct"
theorems dfs_invar_final =
wa_precise_refine.transfer_correctness[OF dfs_pref_sse sse_invar_final]
end