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.9 Sekunden (vorverarbeitet am 2026-06-13) ¤

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.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.