isabelle: src/HOLCF/IOA/Modelcheck/Ring3.thy@62bb8dcc316e (annotated)

7299 743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	1
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	2	Ring3 = MuIOAOracle +
08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	3
08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	4	datatype token = Leader \| id0 \| id1 \| id2 \| id3 \| id4
08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	5
7299 743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	6	datatype Comm =
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	7	Zero_One token \| One_Two token \| Two_Zero token \|
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	8	Leader_Zero \| Leader_One \| Leader_Two
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	9
7299 743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	10	constdefs
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	11	Greater :: [token, token] => bool
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	12	"Greater x y ==
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	13	(x~=Leader & x~=id0 & y=id0) \| (x=id4 & y~=id4 & y~=Leader) \|
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	14	(x=id2 & y=id1) \| (x=id3 & y=id1) \| (x=id3 & y=id2)"
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	15
7299 743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	16
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	17	(the ring is the composition of aut0, aut1 and aut2)
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	18
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	19	automaton aut0 =
7299 743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	20	signature
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	21	actions Comm
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	22	inputs "Two_Zero t"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	23	outputs "Zero_One t","Leader_Zero"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	24	states
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	25	idf :: token
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	26	initially "idf=id0 \| idf = id3"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	27	transitions
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	28	"Two_Zero t"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	29	transrel
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	30	"if (t=id0 \| t=id3) then (idf'=Leader) else
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	31	(if (Greater t idf) then (idf'=t) else (idf'=idf))"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	32	"Zero_One t"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	33	pre "t=idf"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	34	"Leader_Zero"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	35	pre "idf=Leader"
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	36
08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	37	automaton aut1 =
7299 743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	38	signature
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	39	actions Comm
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	40	inputs "Zero_One t"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	41	outputs "One_Two t","Leader_One"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	42	states
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	43	idf :: token
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	44	initially "idf=id1 \| idf=id4"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	45	transitions
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	46	"Zero_One t"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	47	transrel
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	48	"if (t=id1 \| t=id4) then (idf'=Leader) else
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	49	(if (Greater t idf) then (idf'=t) else (idf'=idf))"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	50	"One_Two t"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	51	pre "t=idf"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	52	"Leader_One"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	53	pre "idf=Leader"
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	54
08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	55	automaton aut2 =
7299 743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	56	signature
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	57	actions Comm
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	58	inputs "One_Two t"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	59	outputs "Two_Zero t","Leader_Two"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	60	states
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	61	idf :: token
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	62	initially "idf=id2"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	63	transitions
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	64	"One_Two t"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	65	transrel
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	66	"if (t=id2) then (idf'=Leader) else
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	67	(if (Greater t idf) then (idf'=t) else (idf'=idf))"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	68	"Two_Zero t"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	69	pre "t=idf"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	70	"Leader_Two"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	71	pre "idf=Leader"
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	72
7299 743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	73	automaton ring = compose aut0, aut1, aut2
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	74
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	75
7299 743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	76	(*one_leader expresses property that at most one component declares
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	77	itself to leader*)
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	78
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	79	automaton one_leader =
7299 743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	80	signature
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	81	actions Comm
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	82	outputs "Zero_One t","One_Two t","Two_Zero t","Leader_Zero","Leader_One","Leader_Two"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	83	states
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	84	leader :: token
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	85	initially "leader=Leader"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	86	transitions
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	87	"Zero_One t"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	88	pre "True"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	89	"One_Two t"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	90	pre "True"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	91	"Two_Zero t"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	92	pre "True"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	93	"Leader_Zero"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	94	pre "leader=id0 \| leader=Leader"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	95	post leader:="id0"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	96	"Leader_One"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	97	pre "leader=id1 \| leader=Leader"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	98	post leader:="id1"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	99	"Leader_Two"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	100	pre "leader=id2 \| leader=Leader"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	101	post leader:="id2"
743b22579a2f quite a lot of tuning and cleanup; wenzelm parents: 6471 diff changeset	102
6471 08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	103
08d12ef5fc19 added translation from IOA to mucalculus and corresponding modelchecker examples; mueller parents: diff changeset	104	end

author	wenzelm
	Sat, 03 Sep 2005 16:47:25 +0200
changeset 17241	62bb8dcc316e
parent 7299	743b22579a2f
child 17244	0b2ff9541727
permissions	-rw-r--r--