isabelle: src/HOLCF/IOA/ABP/Env.thy@a34c20f4bf44 (annotated)

3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	1	(* Title: HOLCF/IOA/ABP/Impl.thy
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	2	ID: $Id$
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	3	Author: Olaf Mueller
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	4	Copyright 1995 TU Muenchen
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	5
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	6	The environment
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	7	*)
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	8
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	9	Env = IOA + Action +
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	10
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	11	types
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	12
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	13	'm env_state = "bool"
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	14	(* give next bit to system *)
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	15
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	16	consts
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	17
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	18	env_asig :: 'm action signature
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	19	env_trans :: ('m action, 'm env_state)transition set
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	20	env_ioa :: ('m action, 'm env_state)ioa
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	21	next :: 'm env_state => bool
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	22
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	23	defs
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	24
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	25	env_asig_def
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	26	"env_asig == ({Next},
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	27	UN m. {S_msg(m)},
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	28	{})"
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	29
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	30	env_trans_def "env_trans ==
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	31	{tr. let s = fst(tr);
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	32	t = snd(snd(tr))
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	33	in case fst(snd(tr))
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	34	of
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	35	Next => t=True \|
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	36	S_msg(m) => s=True & t=False \|
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	37	R_msg(m) => False \|
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	38	S_pkt(pkt) => False \|
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	39	R_pkt(pkt) => False \|
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	40	S_ack(b) => False \|
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	41	R_ack(b) => False}"
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	42
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	43	env_ioa_def "env_ioa ==
3522 a34c20f4bf44 changes neede for introducing fairness mueller parents: 3072 diff changeset	44	(env_asig, {True}, env_trans,{},{})"
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	45
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	46	end
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	47

author	mueller
	Thu, 17 Jul 1997 12:44:16 +0200
changeset 3522	a34c20f4bf44
parent 3072	a31419014be5
child 6468	a7b1669f5365
permissions	-rw-r--r--