#Synapse
##Graph generated by single-result supercompiler
The size of graph: 11.
|__List(ω, 0, 0)
|1
|__List(ω, 0, 1)
|1
|__List(ω, 0, ω)
|1
|__List(ω, 0, ω)*
|2
|__List(ω, 1, 0)
|1
|__List(ω, 0, 1)*
|3
|__List(ω, 1, 0)*
|3
|__List(ω, 1, 0)*
|2
|__List(ω, 1, 0)*
|3
|__List(ω, 1, 0)*
|3
|__List(ω, 1, 0)*
##The minimal graph found by multi-result supercompiler
The size of graph: 6.
|__List(ω, 0, ω)
|1
|__List(ω, 0, ω)*
|2
|__List(ω, 1, 0)
|1
|__List(ω, 0, 1)*
|3
|__List(ω, 1, 0)*
|3
|__List(ω, 1, 0)*
##The proof of safety of protocol for Isabelle
theory synapse
imports Main
begin
inductive synapse :: "(nat * nat * nat) => bool" where
"synapse (i, 0, 0)" |
"synapse (Suc i, d, v) ==> synapse (i + d, 0, Suc v)" |
"synapse (i, d, Suc v) ==> synapse (i + d + v, (Suc 0), 0)" |
"synapse (Suc i, d, v) ==> synapse (i + d + v, (Suc 0), 0)"
inductive unsafe :: "(nat * nat * nat) => bool" where
"unsafe (x, Suc y, Suc z)" |
"unsafe (x, Suc (Suc y), z)"
inductive synapse' :: "(nat * nat * nat) => bool" where
"synapse'(_, Suc 0, 0)" |
"synapse'(_, 0, _)"
lemma inclusion: "synapse c ==> synapse' c"
apply(erule synapse.induct)
apply(erule synapse'.cases | simp add: synapse'.intros)+
done
lemma safety: "synapse' c ==> ~unsafe c"
apply(erule synapse'.cases)
apply(erule unsafe.cases | auto)+
done
theorem valid: "synapse c ==> ~unsafe c"
apply(insert inclusion safety, simp)
done
end
#MSI
##Graph generated by single-result supercompiler
The size of graph: 8.
|__List(ω, 0, 0)
|1
|__List(ω, 1, 0)
|1
|__List(ω, 1, 0)*
|3
|__List(ω, 0, ω)
|1
|__List(ω, 1, 0)*
|2
|__List(ω, 1, 0)*
|3
|__List(ω, 0, ω)*
|3
|__List(ω, 0, 1)*
##The minimal graph found by multi-result supercompiler
The size of graph: 6.
|__List(ω, 0, ω)
|1
|__List(ω, 1, 0)
|1
|__List(ω, 1, 0)*
|3
|__List(ω, 0, 2)*
|2
|__List(ω, 1, 0)*
|3
|__List(ω, 0, ω)*
##The proof of safety of protocol for Isabelle
theory msi
imports Main
begin
inductive msi :: "(nat * nat * nat) => bool" where
"msi (i, 0, 0)" |
"msi (Suc i, m, s) ==> msi (i + m + s, Suc 0, 0)" |
"msi (i, m, Suc s) ==> msi (i + m + s, Suc 0, 0)" |
"msi (Suc i, m, s) ==> msi (i, 0, Suc (m + s))"
inductive unsafe :: "(nat * nat * nat) => bool" where
"unsafe (x, Suc y, Suc z)" |
"unsafe (x, Suc (Suc y), z)"
inductive msi' :: "(nat * nat * nat) => bool" where
"msi'(_, 0, _)" |
"msi'(_, Suc 0, 0)"
lemma inclusion: "msi c ==> msi' c"
apply(erule msi.induct)
apply(erule msi'.cases | simp add: msi'.intros)+
done
lemma safety: "msi' c ==> ~unsafe c"
apply(erule msi'.cases)
apply(erule unsafe.cases | auto)+
done
theorem valid: "msi c ==> ~unsafe c"
apply(insert inclusion safety, simp)
done
end
#MOSI
##Graph generated by single-result supercompiler
The size of graph: 26.
|__List(ω, 0, 0, 0)
|1
|__List(ω, 0, 1, 0)
|1
|__List(ω, 0, ω, 0)
|1
|__List(ω, 0, ω, 0)*
|3
|__List(ω, 0, 0, 1)
|1
|__List(ω, 1, 1, 0)
|1
|__List(ω, 1, ω, 0)
|1
|__List(ω, 1, ω, 0)*
|2
|__List(ω, 0, 0, 1)*
|3
|__List(ω, 0, 0, 1)*
|4
|__List(ω, 0, 0, 1)*
|5
|__List(ω, 1, ω, 0)*
|7
|__List(ω, 0, ω, 0)*
|2
|__List(ω, 0, 0, 1)*
|3
|__List(ω, 0, 0, 1)*
|4
|__List(ω, 0, 0, 1)*
|5
|__List(ω, 1, 0, 0)*
|7
|__List(ω, 0, 1, 0)*
|3
|__List(ω, 0, 0, 1)*
|6
|__List(ω, 0, 0, 0)*
|4
|__List(ω, 0, 0, 1)*
|5
|__List(ω, 0, ω, 0)*
|3
|__List(ω, 0, 0, 1)*
|4
|__List(ω, 0, 0, 1)*
|5
|__List(ω, 0, 0, 0)*
|3
|__List(ω, 0, 0, 1)*
##The minimal graph found by multi-result supercompiler
The size of graph: 14.
|__List(ω, 0, ω, 0)
|1
|__List(ω, 0, ω, 0)*
|3
|__List(ω, 0, 0, 1)
|1
|__List(ω, 1, ω, 0)
|1
|__List(ω, 1, ω, 0)*
|2
|__List(ω, 0, 0, 1)*
|3
|__List(ω, 0, 0, 1)*
|4
|__List(ω, 0, 0, 1)*
|5
|__List(ω, 1, ω, 0)*
|7
|__List(ω, 0, ω, 0)*
|3
|__List(ω, 0, 0, 1)*
|6
|__List(ω, 0, 0, 0)*
|4
|__List(ω, 0, 0, 1)*
|5
|__List(ω, 0, ω, 0)*
##The proof of safety of protocol for Isabelle
theory mosi
imports Main
begin
inductive mosi :: "(nat * nat * nat * nat) => bool" where
"mosi (i, 0, 0, 0)" |
"mosi (Suc i, o', s, m) ==> mosi (i, m + o', Suc s, 0)" |
"mosi (i, Suc o', s, m) ==> mosi (i + o' + s + m, 0, 0, Suc 0)" |
"mosi (Suc i, o', s, m) ==> mosi (i + o' + s + m, 0, 0, Suc 0)" |
"mosi (i, o', Suc s, m) ==> mosi (i + o' + s + m, 0, 0, Suc 0)" |
"mosi (i, o', Suc s, m) ==> mosi (Suc i, o', s, m)" |
"mosi (i, o', s, Suc m) ==> mosi (Suc i, o', s, m)" |
"mosi (i, Suc o', s, m) ==> mosi (Suc i, o', s, m)"
inductive unsafe :: "(nat * nat * nat * nat) => bool" where
"unsafe (i, Suc (Suc o'), s, m)" |
"unsafe (i, o', s, Suc (Suc m))" |
"unsafe (i, o', Suc s, Suc m)"
inductive mosi' :: "(nat * nat * nat * nat) => bool" where
"mosi'(_, 0, _, 0)" |
"mosi'(_, 0, 0, Suc 0)" |
"mosi'(_, Suc 0, _, 0)"
lemma inclusion: "mosi c ==> mosi' c"
apply(erule mosi.induct)
apply(erule mosi'.cases | simp add: mosi'.intros)+
done
lemma safety: "mosi' c ==> ~unsafe c"
apply(erule mosi'.cases)
apply(erule unsafe.cases | auto)+
done
theorem valid: "mosi c ==> ~unsafe c"
apply(insert inclusion safety, simp)
done
end
#MESI
##Graph generated by single-result supercompiler
The size of graph: 14.
|__List(ω, 0, 0, 0)
|1
|__List(ω, 0, 1, 0)
|1
|__List(ω, 0, ω, 0)
|1
|__List(ω, 0, ω, 0)*
|3
|__List(ω, 1, 0, 0)
|1
|__List(ω, 0, 2, 0)*
|2
|__List(ω, 0, 0, 1)
|1
|__List(ω, 0, 2, 0)*
|4
|__List(ω, 1, 0, 0)*
|4
|__List(ω, 1, 0, 0)*
|4
|__List(ω, 1, 0, 0)*
|3
|__List(ω, 1, 0, 0)*
|4
|__List(ω, 1, 0, 0)*
|4
|__List(ω, 1, 0, 0)*
##The minimal graph found by multi-result supercompiler
The size of graph: 9.
|__List(ω, 0, ω, 0)
|1
|__List(ω, 0, ω, 0)*
|3
|__List(ω, 1, 0, 0)
|1
|__List(ω, 0, 2, 0)*
|2
|__List(ω, 0, 0, 1)
|1
|__List(ω, 0, 2, 0)*
|4
|__List(ω, 1, 0, 0)*
|4
|__List(ω, 1, 0, 0)*
|4
|__List(ω, 1, 0, 0)*
##The proof of safety of protocol for Isabelle
theory mesi
imports Main
begin
inductive mesi :: "(nat * nat * nat * nat) => bool" where
"mesi (i, 0, 0, 0)" |
"mesi (Suc i, e, s, m) ==> mesi (i, 0, Suc (s + e + m), 0)" |
"mesi (i, Suc e, s, m) ==> mesi (i, e, s, Suc m)" |
"mesi (i, e, Suc s, m) ==> mesi (i + e + s + m, Suc 0, 0, 0)" |
"mesi (Suc i, e, s, m) ==> mesi (i + e + s + m, Suc 0, 0, 0)"
inductive unsafe :: "(nat * nat * nat * nat) => bool" where
"unsafe (i, e, s, Suc (Suc m))" |
"unsafe (i, e, Suc s, Suc m)"
inductive mesi' :: "(nat * nat * nat * nat) => bool" where
"mesi'(_, Suc 0, 0, 0)" |
"mesi'(_, 0, 0, Suc 0)" |
"mesi'(_, 0, _, 0)"
lemma inclusion: "mesi c ==> mesi' c"
apply(erule mesi.induct)
apply(erule mesi'.cases | simp add: mesi'.intros)+
done
lemma safety: "mesi' c ==> ~unsafe c"
apply(erule mesi'.cases)
apply(erule unsafe.cases | auto)+
done
theorem valid: "mesi c ==> ~unsafe c"
apply(insert inclusion safety, simp)
done
end
#MOESI
##Graph generated by single-result supercompiler
The size of graph: 20.
|__List(ω, 0, 0, 0, 0)
|1
|__List(ω, 0, 1, 0, 0)
|1
|__List(ω, 0, ω, 0, 0)
|1
|__List(ω, 0, ω, 0, 0)*
|3
|__List(ω, 0, 0, 1, 0)
|1
|__List(ω, 0, 2, 0, 0)*
|2
|__List(ω, 1, 0, 0, 0)
|1
|__List(ω, 0, 1, 0, 1)
|1
|__List(ω, 0, ω, 0, 1)
|1
|__List(ω, 0, ω, 0, 1)*
|3
|__List(ω, 0, 0, 1, 0)*
|4
|__List(ω, 0, 0, 1, 0)*
|3
|__List(ω, 0, 0, 1, 0)*
|4
|__List(ω, 0, 0, 1, 0)*
|4
|__List(ω, 0, 0, 1, 0)*
|4
|__List(ω, 0, 0, 1, 0)*
|4
|__List(ω, 0, 0, 1, 0)*
|3
|__List(ω, 0, 0, 1, 0)*
|4
|__List(ω, 0, 0, 1, 0)*
|4
|__List(ω, 0, 0, 1, 0)*
##The minimal graph found by multi-result supercompiler
The size of graph: 9.
|__List(ω, 0, ω, 0, ω)
|1
|__List(ω, 0, ω, 0, ω)*
|3
|__List(ω, 0, 0, 1, 0)
|1
|__List(ω, 0, 2, 0, 0)*
|2
|__List(ω, 1, 0, 0, 0)
|1
|__List(ω, 0, 1, 0, 1)*
|4
|__List(ω, 0, 0, 1, 0)*
|4
|__List(ω, 0, 0, 1, 0)*
|4
|__List(ω, 0, 0, 1, 0)*
##The proof of safety of protocol for Isabelle
theory moesi
imports Main
begin
inductive moesi :: "(nat * nat * nat * nat * nat) => bool" where
"moesi (i, 0, 0, 0, 0)" |
"moesi (Suc i, m, s, e, o') ==> moesi (i, 0, Suc (s + e), 0, m + o')" |
"moesi (i, m, s, Suc e, o') ==> moesi (i, Suc m, s, e, o')" |
"moesi (i, m, Suc s, e, o') ==> moesi (i + m + s + e + o', 0, 0, Suc 0, 0)" |
"moesi (Suc i, m, s, e, o') ==> moesi (i + m + s + e + o', 0, 0, Suc 0, 0)"
inductive unsafe :: "(nat * nat * nat * nat * nat) => bool" where
"unsafe (i, Suc m, Suc s, e, o')" |
"unsafe (i, Suc m, s, Suc e, o')" |
"unsafe (i, Suc m, s, e, Suc o')" |
"unsafe (i, Suc (Suc m), s, e, o')" |
"unsafe (i, m, s, Suc (Suc e), o')"
inductive moesi' :: "(nat * nat * nat * nat * nat) => bool" where
"moesi'(_, 0, 0, Suc 0, 0)" |
"moesi'(_, Suc 0, 0, 0, 0)" |
"moesi'(_, 0, _, 0, _)"
lemma inclusion: "moesi c ==> moesi' c"
apply(erule moesi.induct)
apply(erule moesi'.cases | simp add: moesi'.intros)+
done
lemma safety: "moesi' c ==> ~unsafe c"
apply(erule moesi'.cases)
apply(erule unsafe.cases | auto)+
done
theorem valid: "moesi c ==> ~unsafe c"
apply(insert inclusion safety, simp)
done
end
#Illinois
##Graph generated by single-result supercompiler
The size of graph: 15.
|__List(ω, 0, 0, 0)
|1
|__List(ω, 1, 0, 0)
|3
|__List(ω, 0, 0, ω)
|1
|__List(ω, 1, 0, 0)*
|3
|__List(ω, 0, 0, ω)*
|5
|__List(ω, 0, 1, 0)
|2
|__List(ω, 0, 0, 2)*
|6
|__List(ω, 0, 1, 0)*
|7
|__List(ω, 0, 0, 0)*
|6
|__List(ω, 0, 1, 0)*
|8
|__List(ω, 0, 0, ω)*
|4
|__List(ω, 0, 1, 0)*
|6
|__List(ω, 0, 1, 0)*
|9
|__List(ω, 0, 0, 0)*
|6
|__List(ω, 0, 1, 0)*
##The minimal graph found by multi-result supercompiler
The size of graph: 13.
|__List(ω, 0, 0, ω)
|1
|__List(ω, 1, 0, 0)
|3
|__List(ω, 0, 0, 2)*
|4
|__List(ω, 0, 1, 0)
|2
|__List(ω, 0, 0, 2)*
|6
|__List(ω, 0, 1, 0)*
|7
|__List(ω, 0, 0, 0)*
|6
|__List(ω, 0, 1, 0)*
|9
|__List(ω, 0, 0, 0)*
|3
|__List(ω, 0, 0, ω)*
|5
|__List(ω, 0, 1, 0)*
|6
|__List(ω, 0, 1, 0)*
|8
|__List(ω, 0, 0, ω)*
##The proof of safety of protocol for Isabelle
theory illinois
imports Main
begin
inductive illinois :: "(nat * nat * nat * nat) => bool" where
start: "illinois (i, 0, 0, 0)" |
r2: "illinois (Suc i, 0, 0, 0) ==> illinois (i, Suc 0, 0, 0)" |
r3: "illinois (Suc i, e, Suc d, s) ==> illinois (i, e, d, Suc (Suc s))" |
r4a: "illinois (Suc i, Suc e, d, s) ==> illinois (i, 0, d, Suc (s + e))" |
r4b: "illinois (Suc i, e, d, Suc s) ==> illinois (i, 0, d, Suc (s + e))" |
r6: "illinois (i, Suc e, d, s) ==> illinois (i, e, Suc d, s)" |
r7: "illinois (i, e, d, Suc s) ==> illinois (i + s, e, Suc d, 0)" |
r8: "illinois (Suc i, e, d, s) ==> illinois (i + e + d + s, 0, Suc 0, 0)" |
r9: "illinois (i, e, Suc d, s) ==> illinois (Suc i, e, d, s)" |
r10: "illinois (i, e, d, Suc s) ==> illinois (Suc i, e, d, s)" |
r11: "illinois (i, Suc e, d, s) ==> illinois (Suc i, e, d, s)"
inductive unsafe :: "(nat * nat * nat * nat) => bool" where
"unsafe (i, e, Suc d, Suc s)" |
"unsafe (i, e, Suc (Suc d), s)"
inductive illinois' :: "(nat * nat * nat * nat) => bool" where
"illinois'(_, 0, 0, _)" |
"illinois'(_, 0, Suc 0, 0)" |
"illinois'(_, Suc 0, 0, 0)"
lemma inclusion: "illinois c ==> illinois' c"
apply(erule illinois.induct)
apply(erule illinois'.cases | simp add: illinois'.intros)+
done
lemma safety: "illinois' c ==> ~unsafe c"
apply(erule illinois'.cases)
apply(erule unsafe.cases | auto)+
done
theorem valid: "illinois c ==> ~unsafe c"
apply(insert inclusion safety, simp)
done
end
#Berkley
##Graph generated by single-result supercompiler
The size of graph: 17.
|__List(ω, 0, 0, 0)
|1
|__List(ω, 0, 1, 0)
|1
|__List(ω, 0, ω, 0)
|1
|__List(ω, 0, ω, 0)*
|2
|__List(ω, 0, 0, 1)
|1
|__List(ω, 1, 1, 0)
|1
|__List(ω, 1, ω, 0)
|1
|__List(ω, 1, ω, 0)*
|2
|__List(ω, 0, 0, 1)*
|3
|__List(ω, 0, 0, 1)*
|2
|__List(ω, 0, 0, 1)*
|3
|__List(ω, 0, 0, 1)*
|2
|__List(ω, 0, 0, 1)*
|3
|__List(ω, 0, 0, 1)*
|2
|__List(ω, 0, 0, 1)*
|3
|__List(ω, 0, 0, 1)*
|2
|__List(ω, 0, 0, 1)*
##The minimal graph found by multi-result supercompiler
The size of graph: 6.
|__List(ω, ω, ω, 0)
|1
|__List(ω, ω, ω, 0)*
|2
|__List(ω, 0, 0, 1)
|1
|__List(ω, 1, 1, 0)*
|2
|__List(ω, 0, 0, 1)*
|3
|__List(ω, 0, 0, 1)*
##The proof of safety of protocol for Isabelle
theory berkley
imports Main
begin
inductive berkley :: "(nat * nat * nat * nat) => bool" where
start: "berkley (i, 0, 0, 0)" |
rm: "berkley (Suc i, n, u, e) ==> berkley (i, n + e, Suc u, 0)" |
wm: "berkley (Suc i, n, u, e) ==> berkley (i + n + u + e, 0, 0, Suc 0)" |
wh1: "berkley (i, Suc n, u, e) ==> berkley (i + n + u, 0, 0, Suc e)" |
wh2: "berkley (i, n, Suc u, e) ==> berkley (i + n + u, 0, 0, Suc e)"
inductive unsafe :: "(nat * nat * nat * nat) => bool" where
"unsafe (i, Suc n, u, Suc e)" |
"unsafe (i, n, Suc u, Suc e)" |
"unsafe (i, n, u, Suc (Suc e))"
inductive berkley' :: "(nat * nat * nat * nat) => bool" where
"berkley'(_, 0, 0, Suc 0)" |
"berkley'(_, _, _, 0)"
lemma inclusion: "berkley c ==> berkley' c"
apply(erule berkley.induct)
apply(erule berkley'.cases | simp add: berkley'.intros)+
done
lemma safety: "berkley' c ==> ~unsafe c"
apply(erule berkley'.cases)
apply(erule unsafe.cases | auto)+
done
theorem valid: "berkley c ==> ~unsafe c"
apply(insert inclusion safety, simp)
done
end
#Firefly
##Graph generated by single-result supercompiler
The size of graph: 12.
|__List(ω, 0, 0, 0)
|1
|__List(ω, 1, 0, 0)
|3
|__List(ω, 0, ω, 0)
|1
|__List(ω, 1, 0, 0)*
|3
|__List(ω, 0, ω, 0)*
|5
|__List(ω, 1, 0, 0)*
|6
|__List(ω, 0, 0, 1)
|2
|__List(ω, 0, 2, 0)*
|6
|__List(ω, 0, 0, 1)*
|4
|__List(ω, 0, 0, 1)*
|6
|__List(ω, 0, 0, 1)*
|6
|__List(ω, 0, 0, 1)*
##The minimal graph found by multi-result supercompiler
The size of graph: 10.
|__List(ω, 0, ω, 0)
|1
|__List(ω, 1, 0, 0)
|3
|__List(ω, 0, 2, 0)*
|4
|__List(ω, 0, 0, 1)
|2
|__List(ω, 0, 2, 0)*
|6
|__List(ω, 0, 0, 1)*
|6
|__List(ω, 0, 0, 1)*
|3
|__List(ω, 0, ω, 0)*
|5
|__List(ω, 1, 0, 0)*
|6
|__List(ω, 0, 0, 1)*
##The proof of safety of protocol for Isabelle
theory firefly
imports Main
begin
inductive firefly :: "(nat * nat * nat * nat) => bool" where
start: "firefly (i, 0, 0, 0)" |
rm1: "firefly (Suc i, 0, 0, 0) ==> firefly (i, Suc 0, 0, 0)" |
rm2: "firefly (Suc i, e, s, Suc d) ==> firefly (i, e, Suc (Suc s), d)" |
rm31: "firefly (Suc i, Suc e, s, d) ==> firefly (i, 0, Suc (e + s), d)" |
rm32: "firefly (Suc i, e, Suc s, d) ==> firefly (i, 0, Suc (e + s), d)" |
wh2: "firefly (i, Suc e, s, d) ==> firefly (i, e, s, Suc d)" |
wh3: "firefly (i, e, Suc s, d) ==> firefly (i, Suc e, 0, d)" |
wm: "firefly (Suc i, e, s, d) ==> firefly (i + e + s + d, 0, 0, Suc 0)"
inductive unsafe :: "(nat * nat * nat * nat) => bool" where
"unsafe (i, Suc e, s, Suc d)" |
"unsafe (i, e, Suc s, Suc d)" |
"unsafe (i, Suc (Suc e), s, d)" |
"unsafe (i, e, s, Suc (Suc d))"
inductive firefly' :: "(nat * nat * nat * nat) => bool" where
"firefly'(_, 0, 0, Suc 0)" |
"firefly'(_, Suc 0, 0, 0)" |
"firefly'(_, 0, _, 0)"
lemma inclusion: "firefly c ==> firefly' c"
apply(erule firefly.induct)
apply(erule firefly'.cases | simp add: firefly'.intros)+
done
lemma safety: "firefly' c ==> ~unsafe c"
apply(erule firefly'.cases)
apply(erule unsafe.cases | auto)+
done
theorem valid: "firefly c ==> ~unsafe c"
apply(insert inclusion safety, simp)
done
end
#Futurebus
##Graph generated by single-result supercompiler
The size of graph: 45.
|__List(ω, 0, 0, 0, 0, 0, 0, 0, 0)
|1
|__List(ω, 0, 0, 0, 1, 0, 0, 0, 0)
|1
|__List(ω, 0, 0, 0, ω, 0, 0, 0, 0)
|1
|__List(ω, 0, 0, 0, ω, 0, 0, 0, 0)*
|4
|__List(ω, ω, 0, 0, 0, 0, 0, 0, 0)
|1
|__List(ω, 0, 0, 0, 1, 0, 0, 0, ω)
|1
|__List(ω, 0, 0, 0, ω, 0, 0, 0, ω)
|1
|__List(ω, 0, 0, 0, ω, 0, 0, 0, ω)*
|3
|__List(ω, ω, 0, 0, 0, 0, 0, 0, 0)*
|4
|__List(ω, ω, 0, 0, 0, 0, 0, 0, 0)*
|5
|__List(ω, 0, 1, 0, 0, 0, 0, 0, 0)
|1
|__List(ω, 0, 0, 0, 1, 0, 0, 0, 1)*
|6
|__List(ω, 0, 0, 0, 0, 1, 0, 0, 0)
|8
|__List(ω, 0, 0, 1, 0, 0, 0, 0, 0)
|1
|__List(ω, 0, 0, 0, 1, 0, 1, 0, 0)
|1
|__List(ω, 0, 0, 0, ω, 0, 1, 0, 0)
|1
|__List(ω, 0, 0, 0, ω, 0, 1, 0, 0)*
|2
|__List(ω, ω, 0, 0, 0, 0, 0, 0, 0)*
|6
|__List(ω, 0, 0, 0, 0, 1, 0, 0, 0)*
|8
|__List(ω, 0, 0, 0, ω, 0, 1, 0, 0)*
|2
|__List(ω, 2, 0, 0, 0, 0, 0, 0, 0)*
|6
|__List(ω, 0, 0, 0, 0, 1, 0, 0, 0)*
|8
|__List(ω, 0, 0, 0, 1, 0, 1, 0, 0)*
|6
|__List(ω, 0, 0, 0, 0, 1, 0, 1, 0)
|7
|__List(ω, 0, 0, 1, 0, 0, 0, 0, 0)*
|8
|__List(ω, 0, 0, 1, 0, 0, 0, 0, 0)*
|8
|__List(ω, 0, 1, 0, 0, 0, 0, 0, 0)*
|9
|__List(ω, 0, 0, 1, 0, 0, 0, 0, 0)*
|6
|__List(ω, 0, 0, 0, 0, 1, 0, 0, 0)*
|8
|__List(ω, 0, 0, 0, ω, 0, 0, 0, ω)*
|3
|__List(ω, ω, 0, 0, 0, 0, 0, 0, 0)*
|5
|__List(ω, 0, 1, 0, 0, 0, 0, 0, 0)*
|6
|__List(ω, 0, 0, 0, 0, 1, 0, 0, 0)*
|8
|__List(ω, 0, 0, 0, 1, 0, 0, 0, ω)*
|6
|__List(ω, 0, 0, 0, 0, 1, 0, 0, 0)*
|8
|__List(ω, ω, 0, 0, 0, 0, 0, 0, 0)*
|10
|__List(ω, 0, 0, 1, 0, 0, 0, 0, 0)*
|5
|__List(ω, 0, 1, 0, 0, 0, 0, 0, 0)*
|6
|__List(ω, 0, 0, 0, 0, 1, 0, 0, 0)*
|8
|__List(ω, 0, 0, 0, ω, 0, 0, 0, 0)*
|5
|__List(ω, 0, 1, 0, 0, 0, 0, 0, 0)*
|6
|__List(ω, 0, 0, 0, 0, 1, 0, 0, 0)*
|8
|__List(ω, 0, 0, 0, 1, 0, 0, 0, 0)*
|6
|__List(ω, 0, 0, 0, 0, 1, 0, 0, 0)*
|8
|__List(ω, 0, 0, 0, 0, 0, 0, 0, 0)*
##The minimal graph found by multi-result supercompiler
The size of graph: 24.
|__List(ω, ω, 0, 0, 0, 0, 0, 0, 0)
|1
|__List(ω, 0, 0, 0, ω, 0, 0, 0, ω)
|1
|__List(ω, 0, 0, 0, ω, 0, 0, 0, ω)*
|3
|__List(ω, ω, 0, 0, 0, 0, 0, 0, 0)*
|4
|__List(ω, ω, 0, 0, 0, 0, 0, 0, 0)*
|5
|__List(ω, 0, 1, 0, 0, 0, 0, 0, 0)
|1
|__List(ω, 0, 0, 0, 1, 0, 0, 0, 1)*
|6
|__List(ω, 0, 0, 0, 0, 1, 0, 0, 0)
|8
|__List(ω, 0, 0, 1, 0, 0, 0, 0, 0)
|1
|__List(ω, 0, 0, 0, ω, 0, 1, 0, 0)
|1
|__List(ω, 0, 0, 0, ω, 0, 1, 0, 0)*
|2
|__List(ω, ω, 0, 0, 0, 0, 0, 0, 0)*
|6
|__List(ω, 0, 0, 0, 0, 1, 0, 0, 0)*
|8
|__List(ω, 0, 0, 0, ω, 0, 1, 0, 0)*
|6
|__List(ω, 0, 0, 0, 0, 1, 0, 1, 0)
|7
|__List(ω, 0, 0, 1, 0, 0, 0, 0, 0)*
|8
|__List(ω, 0, 0, 1, 0, 0, 0, 0, 0)*
|8
|__List(ω, 0, 1, 0, 0, 0, 0, 0, 0)*
|9
|__List(ω, 0, 0, 1, 0, 0, 0, 0, 0)*
|6
|__List(ω, 0, 0, 0, 0, 1, 0, 0, 0)*
|8
|__List(ω, 0, 0, 0, ω, 0, 0, 0, ω)*
|6
|__List(ω, 0, 0, 0, 0, 1, 0, 0, 0)*
|8
|__List(ω, ω, 0, 0, 0, 0, 0, 0, 0)*
|10
|__List(ω, 0, 0, 1, 0, 0, 0, 0, 0)*
##The proof of safety of protocol for Isabelle
theory futurebus
imports Main
begin
inductive futurebus :: "(nat * nat * nat * nat * nat * nat * nat * nat * nat) => bool" where
start: "futurebus (i, 0, 0, 0, 0, 0, 0, 0, 0)" |
r2: "futurebus (Suc i, sU, eU, eM, pR, 0, pEMR, pEMW, pSU) ==> futurebus (i, 0, 0, 0, Suc pR, 0, pEMR + eM, pEMW, pSU + sU + eU)" |
r3: "futurebus (i, sU, eU, eM, pR, pW, Suc pEMR, pEMW, pSU) ==> futurebus (i, Suc (sU + pR), eU, eM, 0, pW, pEMR, pEMW, pSU)" |
r4: "futurebus (i, sU, eU, eM, pR, pW, pEMR, pEMW, Suc pSU) ==> futurebus (i, Suc (sU + pR + pSU), eU, eM, 0, pW, pEMR, pEMW, 0)" |
r5: "futurebus (i, sU, eU, eM, Suc (Suc pR), pW, 0, pEMW, 0) ==> futurebus (i, Suc (Suc (sU + pR)), eU, eM, 0, pW, 0, pEMW, 0)" |
r6: "futurebus (i, sU, eU, eM, Suc (Suc 0), pW, 0, pEMW, 0) ==> futurebus (i, sU, Suc eU, eM, 0, pW, 0, pEMW, 0)" |
wm1: "futurebus (Suc i, sU, eU, eM, pR, 0, pEMR, pEMW, pSU) ==> futurebus (i + eU + sU + pSU + pR + pEMR, 0, 0, 0, 0, Suc 0, 0, pEMW + eM, 0)" |
wm2: "futurebus (i, sU, eU, eM, pR, pW, pEMR, Suc pEMW, pSU) ==> futurebus (Suc i, sU, eU, eM + pW, pR, 0, pEMR, pEMW, pSU)" |
wm3: "futurebus (i, sU, eU, eM, pR, pW, pEMR, 0, pSU) ==> futurebus (i, sU, eU, eM + pW, pR, 0, pEMR, 0, pSU)" |
wh2: "futurebus (i, sU, Suc eU, eM, pR, pW, pEMR, pEMW, pSU) ==> futurebus (i, sU, eU, Suc eM, pR, pW, pEMR, pEMW, pSU)" |
wh3: "futurebus (i, Suc sU, eU, eM, pR, pW, pEMR, pEMW, pSU) ==> futurebus (i + sU, 0, eU, Suc eM, pR, pW, pEMR, pEMW, pSU)"
inductive unsafe :: "(nat * nat * nat * nat * nat * nat * nat * nat * nat) => bool" where
"unsafe (i, Suc sU, Suc eU, eM, pR, pW, pEMR, pEMW, pSU)" |
"unsafe (i, Suc sU, eU, Suc eM, pR, pW, pEMR, pEMW, pSU)" |
"unsafe (i, sU, Suc (Suc eU), eM, pR, pW, pEMR, pEMW, pSU)" |
"unsafe (i, sU, eU, Suc (Suc eM), pR, pW, pEMR, pEMW, pSU)" |
"unsafe (i, sU, Suc eU, Suc eM, pR, pW, pEMR, pEMW, pSU)" |
"unsafe (i, sU, eU, eM, Suc pR, Suc pW, pEMR, pEMW, pSU)" |
"unsafe (i, sU, eU, eM, pR, Suc (Suc pW), pEMR, pEMW, pSU)"
inductive futurebus' :: "(nat * nat * nat * nat * nat * nat * nat * nat * nat) => bool" where
"futurebus'(_, 0, 0, Suc 0, 0, 0, 0, 0, 0)" |
"futurebus'(_, _, 0, 0, 0, 0, 0, 0, 0)" |
"futurebus'(_, 0, 0, 0, 0, Suc 0, 0, 0, 0)" |
"futurebus'(_, 0, 0, 0, _, 0, 0, 0, _)" |
"futurebus'(_, 0, Suc 0, 0, 0, 0, 0, 0, 0)" |
"futurebus'(_, 0, 0, 0, 0, Suc 0, 0, Suc 0, 0)" |
"futurebus'(_, 0, 0, 0, _, 0, Suc 0, 0, 0)"
lemma inclusion: "futurebus c ==> futurebus' c"
apply(erule futurebus.induct)
apply(erule futurebus'.cases | simp add: futurebus'.intros)+
done
lemma safety: "futurebus' c ==> ~unsafe c"
apply(erule futurebus'.cases)
apply(erule unsafe.cases | auto)+
done
theorem valid: "futurebus c ==> ~unsafe c"
apply(insert inclusion safety, simp)
done
end
#Xerox
##Graph generated by single-result supercompiler
The size of graph: 22.
|__List(ω, 0, 0, 0, 0)
|1
|__List(ω, 0, 0, 0, 1)
|2
|__List(ω, ω, 0, 0, 0)
|1
|__List(ω, 0, 0, 0, 1)*
|2
|__List(ω, ω, 0, 0, 0)*
|3
|__List(ω, 0, 0, 1, 0)
|2
|__List(ω, 1, 1, 0, 0)
|2
|__List(ω, ω, 1, 0, 0)
|2
|__List(ω, ω, 1, 0, 0)*
|4
|__List(ω, ω, 1, 0, 0)*
|6
|__List(ω, ω, 1, 0, 0)*
|7
|__List(ω, ω, 0, 0, 0)*
|4
|__List(ω, 3, 1, 0, 0)*
|6
|__List(ω, 0, 1, 0, 0)*
|7
|__List(ω, 1, 0, 0, 0)*
|4
|__List(ω, 2, 0, 0, 0)*
|5
|__List(ω, 0, 0, 0, 0)*
|4
|__List(ω, ω, 0, 0, 0)*
|6
|__List(ω, ω, 0, 0, 0)*
|4
|__List(ω, 2, 0, 0, 0)*
|8
|__List(ω, 0, 0, 0, 0)*
|3
|__List(ω, 0, 0, 1, 0)*
##The minimal graph found by multi-result supercompiler
The size of graph: 13.
|__List(ω, ω, ω, 0, 0)
|1
|__List(ω, 0, 0, 0, 1)
|2
|__List(ω, 2, 0, 0, 0)*
|4
|__List(ω, 2, 0, 0, 0)*
|8
|__List(ω, 0, 0, 0, 0)*
|2
|__List(ω, ω, ω, 0, 0)*
|3
|__List(ω, 0, 0, 1, 0)
|2
|__List(ω, 1, 1, 0, 0)*
|4
|__List(ω, 2, 0, 0, 0)*
|5
|__List(ω, 0, 0, 0, 0)*
|4
|__List(ω, ω, ω, 0, 0)*
|6
|__List(ω, ω, ω, 0, 0)*
|7
|__List(ω, ω, ω, 0, 0)*
##The proof of safety of protocol for Isabelle
theory xerox
imports Main
begin
inductive xerox :: "(nat * nat * nat * nat * nat) => bool" where
start: "xerox (i, 0, 0, 0, 0)" |
rm1: "xerox (Suc i, 0, 0, 0, 0) ==> xerox (i, 0, 0, 0, Suc 0)" |
rm2a: "xerox (Suc i, Suc sc, sd, d, e) ==> xerox (i, Suc (sc + e), sd + d, 0, 0)" |
rm2b: "xerox (Suc i, sc, Suc sd, d, e) ==> xerox (i, Suc (sc + e), sd + d, 0, 0)" |
rm2c: "xerox (Suc i, sc, sd, Suc d, e) ==> xerox (i, Suc (sc + e), sd + d, 0, 0)" |
rm2d: "xerox (Suc i, sc, sd, d, Suc e) ==> xerox (i, Suc (sc + e), sd + d, 0, 0)" |
wm1: "xerox (Suc i, 0, 0, 0, 0) ==> xerox (i, 0, 0, Suc 0, 0)" |
wm2a: "xerox (Suc i, Suc sc, sd, d, e) ==> xerox (i, Suc (sc + d + sd), sd, 0, 0)" |
wm2b: "xerox (Suc i, sc, Suc sd, d, e) ==> xerox (i, Suc (sc + d + sd), sd, 0, 0)" |
wm2c: "xerox (Suc i, sc, sd, Suc d, e) ==> xerox (i, Suc (sc + d + sd), sd, 0, 0)" |
wm2d: "xerox (Suc i, sc, sd, d, Suc e) ==> xerox (i, Suc (sc + d + sd), sd, 0, 0)" |
wh1: "xerox (i, sc, sd, Suc d, e) ==> xerox (Suc i, sc, sd, d, e)" |
wh2: "xerox (i, Suc sc, sd, d, e) ==> xerox (Suc i, sc, sd, d, e)" |
wh3: "xerox (i, sc, Suc sd, d, e) ==> xerox (Suc i, sc, sd, d, e)" |
wh4: "xerox (i, sc, sd, d, Suc e) ==> xerox (Suc i, sc, sd, d, e)"
inductive unsafe :: "(nat * nat * nat * nat * nat) => bool" where
"unsafe (i, Suc sc, sd, Suc d, e)" |
"unsafe (i, sc, Suc sd, Suc d, e)" |
"unsafe (i, sc, sd, Suc d, Suc e)" |
"unsafe (i, Suc sc, sd, d, Suc e)" |
"unsafe (i, sc, Suc sd, d, Suc e)" |
"unsafe (i, sc, sd, Suc (Suc d), e)" |
"unsafe (i, sc, sd, d, Suc (Suc e))"
inductive xerox' :: "(nat * nat * nat * nat * nat) => bool" where
"xerox'(_, _, _, 0, 0)" |
"xerox'(_, 0, 0, Suc 0, 0)" |
"xerox'(_, 0, 0, 0, Suc 0)"
lemma inclusion: "xerox c ==> xerox' c"
apply(erule xerox.induct)
apply(erule xerox'.cases | simp add: xerox'.intros)+
done
lemma safety: "xerox' c ==> ~unsafe c"
apply(erule xerox'.cases)
apply(erule unsafe.cases | auto)+
done
theorem valid: "xerox c ==> ~unsafe c"
apply(insert inclusion safety, simp)
done
end
#Java
##Graph generated by single-result supercompiler
The size of graph: 35.
|__List(1, -1, ω, 0, 0, 0, 0, 0)
|1
|__List(0, -1, ω, 0, 1, 0, 0, 0)
|2
|__List(1, -1, ω, 0, 0, 0, 0, 0)*
|3
|__List(0, -1, ω, 1, 1, 1, 0, 0)
|3
|__List(0, -1, ω, ω, 1, ω, 0, 0)
|2
|__List(1, -1, ω, ω, 0, ω, 0, 0)
|1
|__List(0, -1, ω, 0, 1, ω, 0, 0)*
|5
|__List(1, -2, ω, ω, 0, ω, 0, 1)
|1
|__List(0, -2, ω, 0, 1, ω, 0, 1)
|2
|__List(1, -2, ω, 0, 0, ω, 0, 1)*
|3
|__List(0, -2, ω, 1, 1, ω, 0, 1)
|3
|__List(0, -2, ω, ω, 1, ω, 0, 1)
|2
|__List(1, -2, ω, ω, 0, ω, 0, 1)*
|3
|__List(0, -2, ω, ω, 1, ω, 0, 1)*
|4
|__List(0, -2, ω, ω, 0, ω, 1, 1)
|3
|__List(0, -2, ω, ω, 0, ω, 1, 1)*
|8
|__List(0, -4, ω, ω, 0, ω, 0, 1)
|3
|__List(0, -4, ω, ω, 0, ω, 0, 1)*
|9
|__List(0, -4, ω, ω, 1, ω, 0, 0)
|2
|__List(1, -4, ω, ω, 0, ω, 0, 0)
|1
|__List(0, -4, ω, 0, 1, ω, 0, 0)*
|3
|__List(0, -4, ω, ω, 1, ω, 0, 0)*
|4
|__List(0, -4, ω, ω, 0, ω, 1, 0)
|3
|__List(0, -4, ω, ω, 0, ω, 1, 0)*
|4
|__List(0, -2, ω, 0, 0, ω, 1, 1)*
|3
|__List(0, -1, ω, ω, 1, ω, 0, 0)*
|4
|__List(0, -1, ω, ω, 0, ω, 1, 0)
|3
|__List(0, -1, ω, ω, 0, ω, 1, 0)*
|5
|__List(0, -2, ω, ω, 0, ω, 1, 1)*
|7
|__List(0, -3, ω, ω, 0, ω, 0, 0)
|3
|__List(0, -3, ω, ω, 0, ω, 0, 0)*
|6
|__List(0, -4, ω, ω, 0, ω, 0, 1)*
|5
|__List(0, -2, ω, ω, 1, ω, 0, 1)*
|4
|__List(0, -1, ω, 0, 0, 1, 1, 0)*
|5
|__List(0, -2, ω, 1, 1, 0, 0, 1)*
##The minimal graph found by multi-result supercompiler
The size of graph: 25.
|__List(1, -1, ω, ω, 0, ω, 0, 0)
|1
|__List(0, -1, ω, ω, 1, ω, 0, 0)
|2
|__List(1, -1, ω, ω, 0, ω, 0, 0)*
|3
|__List(0, -1, ω, ω, 1, ω, 0, 0)*
|4
|__List(0, -1, ω, ω, 0, ω, 1, 0)
|3
|__List(0, -1, ω, ω, 0, ω, 1, 0)*
|5
|__List(0, -2, ω, ω, 0, ω, 1, 1)
|3
|__List(0, -2, ω, ω, 0, ω, 1, 1)*
|8
|__List(0, -4, ω, ω, 0, ω, 0, 1)
|3
|__List(0, -4, ω, ω, 0, ω, 0, 1)*
|9
|__List(0, -4, ω, ω, 1, ω, 0, 0)
|2
|__List(1, -4, ω, ω, 0, ω, 0, 0)
|1
|__List(0, -4, ω, 0, 1, ω, 0, 0)*
|3
|__List(0, -4, ω, ω, 1, ω, 0, 0)*
|4
|__List(0, -4, ω, ω, 0, ω, 1, 0)
|3
|__List(0, -4, ω, ω, 0, ω, 1, 0)*
|7
|__List(0, -3, ω, ω, 0, ω, 0, 0)
|3
|__List(0, -3, ω, ω, 0, ω, 0, 0)*
|6
|__List(0, -4, ω, ω, 0, ω, 0, 1)*
|5
|__List(0, -2, ω, ω, 1, ω, 0, 1)
|2
|__List(1, -2, ω, ω, 0, ω, 0, 1)
|1
|__List(0, -2, ω, 0, 1, ω, 0, 1)*
|3
|__List(0, -2, ω, ω, 1, ω, 0, 1)*
|4
|__List(0, -2, ω, ω, 0, ω, 1, 1)*
|5
|__List(1, -2, ω, ω, 0, ω, 0, 1)*
##The proof of safety of protocol for Isabelle
theory java
imports Main
begin
inductive java :: "(nat * nat * nat * nat * nat * nat * nat * nat) => bool" where
start: "java (Suc 0, Suc 0, i, 0, 0, 0, 0, 0)" |
getf: "java (Suc 0, race, Suc i, b, o', in', out, w) ==> java (0, race, i, 0, Suc o', in', out, w)" |
putf: "java (0, race, i, 0, Suc o', in', out, w) ==> java (Suc 0, race, Suc i, 0, o', in', out, w)" |
gets: "java (0, race, Suc i, b, o', in', out, w) ==> java (0, race, i, Suc b, o', Suc in', out, w)" |
puts: "java (0, race, i, Suc b, Suc o', in', out, w) ==> java (0, race, i, b, o', in', Suc out, w)" |
req1: "java (nb, Suc 0, i, b, o', Suc in', out, w) ==> java (nb, Suc (Suc 0), i, b, o', in', out, Suc w)" |
req2: "java (nb, Suc (Suc (Suc 0)), i, b, o', Suc in', out, w) ==> java (nb, Suc (Suc (Suc (Suc 0))), i, b, o', in', out, Suc w)" |
rel1: "java (nb, Suc 0, i, b, o', in', Suc out, w) ==> java (nb, Suc (Suc (Suc 0)), Suc i, b, o', in', out, w)" |
rel2: "java (nb, Suc (Suc 0), i, b, o', in', Suc out, w) ==> java (nb, Suc (Suc (Suc (Suc 0))), Suc i, b, o', in', out, w)" |
go: "java (nb, Suc (Suc (Suc (Suc 0))), i, b, o', in', out, Suc w) ==> java (nb, Suc (Suc (Suc (Suc 0))), Suc i, b, Suc o', in', out, w)"
inductive unsafe :: "(nat * nat * nat * nat * nat * nat * nat * nat) => bool" where
"unsafe (nb, race, i, b, Suc (Suc o'), in', out, w)" |
"unsafe (nb, race, i, b, Suc o', in', Suc out, w)" |
"unsafe (nb, race, i, b, o', in', Suc (Suc out), w)"
inductive java' :: "(nat * nat * nat * nat * nat * nat * nat * nat) => bool" where
"java'(Suc 0, Suc (Suc 0), _, _, 0, _, 0, Suc 0)" |
"java'(0, Suc (Suc 0), _, _, 0, _, Suc 0, Suc 0)" |
"java'(0, Suc (Suc 0), _, _, Suc 0, _, 0, Suc 0)" |
"java'(0, Suc (Suc (Suc (Suc 0))), _, _, 0, _, 0, Suc 0)" |
"java'(0, Suc (Suc (Suc 0)), _, _, 0, _, 0, 0)" |
"java'(0, Suc (Suc (Suc (Suc 0))), _, _, 0, _, Suc 0, 0)" |
"java'(0, Suc (Suc (Suc (Suc 0))), _, _, Suc 0, _, 0, 0)" |
"java'(Suc 0, Suc (Suc (Suc (Suc 0))), _, _, 0, _, 0, 0)" |
"java'(0, Suc 0, _, _, 0, _, Suc 0, 0)" |
"java'(0, Suc 0, _, _, Suc 0, _, 0, 0)" |
"java'(Suc 0, Suc 0, _, _, 0, _, 0, 0)"
lemma inclusion: "java c ==> java' c"
apply(erule java.induct)
apply(erule java'.cases | simp add: java'.intros)+
done
lemma safety: "java' c ==> ~unsafe c"
apply(erule java'.cases)
apply(erule unsafe.cases | auto)+
done
theorem valid: "java c ==> ~unsafe c"
apply(insert inclusion safety, simp)
done
end
#ReaderWriter
##Graph generated by single-result supercompiler
The size of graph: 48.
|__List(1, 0, 0, ω, 0, 0)
|5
|__List(1, 0, 0, ω, 1, 0)
|2
|__List(1, 0, 1, ω, 0, 0)
|4
|__List(1, 0, 0, ω, 0, 0)*
|5
|__List(1, 0, 1, ω, 1, 0)
|2
|__List(1, 0, ω, ω, 0, 0)
|4
|__List(1, 0, ω, ω, 0, 0)*
|5
|__List(1, 0, ω, ω, 1, 0)
|2
|__List(1, 0, ω, ω, 0, 0)*
|4
|__List(1, 0, ω, ω, 1, 0)*
|5
|__List(1, 0, ω, ω, ω, 0)
|2
|__List(1, 0, ω, ω, ω, 0)*
|4
|__List(1, 0, ω, ω, ω, 0)*
|5
|__List(1, 0, ω, ω, ω, 0)*
|6
|__List(1, 0, ω, ω, ω, 1)
|1
|__List(0, 1, 0, ω, ω, 1)
|3
|__List(1, 0, 0, ω, ω, 1)*
|5
|__List(0, 1, 0, ω, ω, 1)*
|6
|__List(0, 1, 0, ω, ω, ω)
|3
|__List(1, 0, 0, ω, ω, ω)
|1
|__List(0, 1, 0, ω, ω, ω)*
|2
|__List(1, 0, 1, ω, ω, ω)
|2
|__List(1, 0, ω, ω, ω, ω)
|1
|__List(0, 1, 0, ω, ω, ω)*
|2
|__List(1, 0, ω, ω, ω, ω)*
|4
|__List(1, 0, ω, ω, ω, ω)*
|5
|__List(1, 0, ω, ω, ω, ω)*
|6
|__List(1, 0, ω, ω, ω, ω)*
|4
|__List(1, 0, 0, ω, ω, ω)*
|5
|__List(1, 0, 1, ω, ω, ω)*
|6
|__List(1, 0, 1, ω, ω, ω)*
|5
|__List(1, 0, 0, ω, ω, ω)*
|6
|__List(1, 0, 0, ω, ω, ω)*
|5
|__List(0, 1, 0, ω, ω, ω)*
|6
|__List(0, 1, 0, ω, ω, ω)*
|2
|__List(1, 0, ω, ω, ω, 1)*
|4
|__List(1, 0, ω, ω, ω, 1)*
|5
|__List(1, 0, ω, ω, ω, 1)*
|6
|__List(1, 0, ω, ω, ω, 2)*
|6
|__List(1, 0, ω, ω, 1, 1)*
|6
|__List(1, 0, ω, ω, 0, 1)*
|4
|__List(1, 0, 0, ω, 1, 0)*
|5
|__List(1, 0, 1, ω, 2, 0)*
|6
|__List(1, 0, 1, ω, 1, 1)*
|6
|__List(1, 0, 1, ω, 0, 1)*
|5
|__List(1, 0, 0, ω, 2, 0)*
|6
|__List(1, 0, 0, ω, 1, 1)*
|6
|__List(1, 0, 0, ω, 0, 1)*
##The minimal graph found by multi-result supercompiler
The size of graph: 9.
|__List(1, 0, ω, ω, ω, ω)
|1
|__List(0, 1, 0, ω, ω, ω)
|3
|__List(1, 0, 0, ω, ω, ω)*
|5
|__List(0, 1, 0, ω, ω, ω)*
|6
|__List(0, 1, 0, ω, ω, ω)*
|2
|__List(1, 0, ω, ω, ω, ω)*
|4
|__List(1, 0, ω, ω, ω, ω)*
|5
|__List(1, 0, ω, ω, ω, ω)*
|6
|__List(1, 0, ω, ω, ω, ω)*
##The proof of safety of protocol for Isabelle
theory rw
imports Main
begin
inductive rw :: "(nat * nat * nat * nat * nat * nat) => bool" where
start: "rw (Suc 0, 0, 0, x5, 0, 0)" |
r1: "rw (Suc x2, x3, 0, x5, x6, Suc x7) ==> rw (x2, Suc x3, 0, x5, x6, Suc x7)" |
r2: "rw (Suc x2, x3, x4, x5, Suc x6, x7) ==> rw (Suc x2, x3, Suc x4, x5, x6, x7)" |
r3: "rw (x2, Suc x3, x4, x5, x6, x7) ==> rw (Suc x2, x3, x4, Suc x5, x6, x7)" |
r4: "rw (x2, x3, Suc x4, x5, x6, x7) ==> rw (x2, x3, x4, Suc x5, x6, x7)" |
r5: "rw (x2, x3, x4, Suc x5, x6, x7) ==> rw (x2, x3, x4, x5, Suc x6, x7)" |
r6: "rw (x2, x3, x4, Suc x5, x6, x7) ==> rw (x2, x3, x4, x5, x6, Suc x7)"
inductive unsafe :: "(nat * nat * nat * nat * nat * nat) => bool" where
"unsafe (x2, Suc x3, Suc x4, x5, x6, x7)"
inductive rw' :: "(nat * nat * nat * nat * nat * nat) => bool" where
"rw'(Suc 0, 0, _, _, _, _)" |
"rw'(0, Suc 0, 0, _, _, _)"
lemma inclusion: "rw c ==> rw' c"
apply(erule rw.induct)
apply(erule rw'.cases | simp add: rw'.intros)+
done
lemma safety: "rw' c ==> ~unsafe c"
apply(erule rw'.cases)
apply(erule unsafe.cases | auto)+
done
theorem valid: "rw c ==> ~unsafe c"
apply(insert inclusion safety, simp)
done
end
#DataRace
##Graph generated by single-result supercompiler
The size of graph: 9.
|__List(ω, 0, 0)
|1
|__List(ω, 1, 0)
|3
|__List(ω, 0, 0)*
|2
|__List(ω, 0, 1)
|2
|__List(ω, 0, ω)
|1
|__List(ω, 1, 0)*
|2
|__List(ω, 0, ω)*
|4
|__List(ω, 0, ω)*
|4
|__List(ω, 0, 0)*
##The minimal graph found by multi-result supercompiler
The size of graph: 5.
|__List(ω, 0, ω)
|1
|__List(ω, 1, 0)
|3
|__List(ω, 0, 0)*
|2
|__List(ω, 0, ω)*
|4
|__List(ω, 0, ω)*
##The proof of safety of protocol for Isabelle
theory datarace
imports Main
begin
inductive datarace :: "(nat * nat * nat) => bool" where
"datarace (out, 0, 0)" |
"datarace (Suc out, 0, 0) ==> datarace (out, Suc 0, 0)" |
"datarace (Suc out, 0, scs) ==> datarace (out, 0, Suc scs)" |
"datarace (out, Suc cs, scs) ==> datarace (Suc out, cs, scs)" |
"datarace (out, cs, Suc scs) ==> datarace (Suc out, cs, scs)"
inductive unsafe :: "(nat * nat * nat) => bool" where
"unsafe (out, Suc cs, Suc scs)"
inductive datarace' :: "(nat * nat * nat) => bool" where
"datarace'(_, 0, _)" |
"datarace'(_, Suc 0, 0)"
lemma inclusion: "datarace c ==> datarace' c"
apply(erule datarace.induct)
apply(erule datarace'.cases | simp add: datarace'.intros)+
done
lemma safety: "datarace' c ==> ~unsafe c"
apply(erule datarace'.cases)
apply(erule unsafe.cases | auto)+
done
theorem valid: "datarace c ==> ~unsafe c"
apply(insert inclusion safety, simp)
done
end