Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma

Benutzer


products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Statecharts/ Datei vom 31.4.2026 mit Größe 4 kB

Quelle HAKripke.thy

Sprache: Isabelle

(*  Title:      statecharts/HA/HAKripke.thy

    Author:     Steffen Helke, Software Engineering Group
    Copyright   2010 Technische Universitaet Berlin
*)

section ‹
HAKripke
HASem Kripke

('s,'e,'d)hakripke = "(('s,'e,'d)status,('s,'e,'d)atomar)kripke"
('s,'e,'d)hactl = "(('s,'e,'d)status,('s,'e,'d)atomar)ctl"

LabelFunSem :: "('s,'e,'d)hierauto
=> (('s,'e,'d)status ⇀ ((('s,'e,'d) atomar) set))" where
"LabelFunSem a = (λ ST.
(if (HA ST = a) then
(let
In_preds = (λ s. (IN s)) ` (Conf ST);
En_preds = (λ e. (EN e)) ` (Events ST);
Val_preds = { x . (∃ P. (x = (VAL P)) ∧ P (Value ST)) }
in
Some (In_preds ∪ En_preds ∪ Val_preds ∪ {atomar.TRUE}))
else
None))"

HA2Kripke :: "('s,'e,'d)hierauto => ('s,'e,'d)hakripke" where
"HA2Kripke a =
Abs_kripke ({ST. HA ST = a},
{InitStatus a},
StepRelSem a,
LabelFunSem a)"

eval_ctl_HA :: "[('s,'e,'d)hierauto, ('s,'e,'d)hactl]
=> bool" (‹

"eval_ctl_HA a f = ((HA2Kripke a), (InitStatus a) |=c= f)"

Kripke_HA [simp]:
"Kripke {ST. HA ST = a} {InitStatus a} (StepRelSem a) (LabelFunSem a)"
(unfold Kripke_def)
auto
(unfold StepRelSem_def)
auto
(unfold LabelFunSem_def Let_def If_def dom_def)
auto
2
(rename_tac ST S)
(case_tac "HA ST = a")
auto
(rename_tac ST)
(case_tac "HPT ST = {}")
auto
(rename_tac TSS)
(erule_tac x="StepStatus ST TSS (@ u. u : ResolveRacing TSS)" in allE)
(erule_tac x=TSS in ballE)
auto

LabelFun_LabelFunSem [simp]:
"(LabelFun (HA2Kripke a)) = (LabelFunSem a)"
(unfold HA2Kripke_def LabelFun_def)
auto
(subst Abs_kripke_inverse)
auto
(unfold kripke_def)
auto

InitStatuses_InitStatus [simp]:
"(InitStatuses (HA2Kripke a)) = {(InitStatus a)}"
(unfold HA2Kripke_def InitStatuses_def)
simp
(subst Abs_kripke_inverse)
(unfold kripke_def)
auto

Statuses_StatusesOfHA [simp]:
"(Statuses (HA2Kripke a)) = {ST. HA ST = a}"
(unfold HA2Kripke_def Statuses_def)
simp
(subst Abs_kripke_inverse)
(unfold kripke_def)
auto

StepRel_StepRelSem [simp]:
"(StepRel (HA2Kripke a)) = (StepRelSem a)"
(unfold HA2Kripke_def StepRel_def)
simp
(subst Abs_kripke_inverse)
(unfold kripke_def)
auto

TRUE_LabelFunSem [simp]:
"atomar.TRUE ∈ the (LabelFunSem (HA ST) ST)"
(unfold LabelFunSem_def Let_def)
auto

FALSE_LabelFunSem [simp]:
"atomar.FALSE ∉ the (LabelFunSem (HA ST) ST)"
(unfold LabelFunSem_def Let_def)
auto

Conf_LabelFunSem [simp]:
"((IN S) ∈ the (LabelFunSem (HA ST) ST)) = (S ∈ (Conf ST))"
(unfold LabelFunSem_def Let_def)
auto

Events_LabelFunSem [simp]:
"((EN S) ∈ the (LabelFunSem (HA ST) ST)) = (S ∈ (Events ST))"
(unfold LabelFunSem_def Let_def)
auto

Value_LabelFunSem [simp]:
"((VAL P) ∈ the (LabelFunSem (HA ST) ST)) = (P (Value ST))"
(unfold LabelFunSem_def Let_def)
auto

AtomTRUE_EvalCTLHA [simp]:
"a |=H= (Atom (atomar.TRUE))"
(unfold eval_ctl_HA_def)
auto
(subst HA_InitStatus [THEN sym])
(rule TRUE_LabelFunSem)

AtomFalse_EvalCTLHA [simp]:
"¬
(unfold eval_ctl_HA_def)
auto
(subst (asm) HA_InitStatus [THEN sym])
(simp only: FALSE_LabelFunSem)

Events_InitStatus_EvalCTLHA [simp]:
"(a |=H= (Atom (EN S))) = (S ∈ (Events (InitStatus a)))"
(unfold eval_ctl_HA_def)
simp
(subst HA_InitStatus [THEN sym])
(rule Events_LabelFunSem)

Conf_InitStatus_EvalCTLHA [simp]:
"(a |=H= (Atom (IN S))) = (S ∈ (Conf (InitStatus a)))"
(unfold eval_ctl_HA_def)
simp
(subst HA_InitStatus [THEN sym])
(subst Conf_LabelFunSem)
simp

HAInitValue_EvalCTLHA [simp]:
"(a |=H= (Atom (VAL P))) = (P (HAInitValue a))"
(unfold eval_ctl_HA_def)
simp
(subst HA_InitStatus [THEN sym])
(subst Value_LabelFunSem)
auto

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.2 Sekunden ¤

Wurzel

Suchen

NIST Cobol Testsuite

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.