From ab4627f7d91578cb373f7c2d5b03e8b7380d11a7 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Tue, 20 Dec 2022 10:42:36 +0100
Subject: [PATCH] add Event-B models for SKS
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
sks/models/empty_ctx.eventb | 2 ++
sks/models/m0_3cars.eventb | 2 ++
sks/models/train_ctx0_beebook_ctx.eventb | 2 ++
3 files changed, 6 insertions(+)
create mode 100644 sks/models/empty_ctx.eventb
create mode 100644 sks/models/m0_3cars.eventb
create mode 100644 sks/models/train_ctx0_beebook_ctx.eventb
diff --git a/sks/models/empty_ctx.eventb b/sks/models/empty_ctx.eventb
new file mode 100644
index 0000000..93638ea
--- /dev/null
+++ b/sks/models/empty_ctx.eventb
@@ -0,0 +1,2 @@
+package(load_event_b_project([],[event_b_context(none,empty,[extends(none,[]),constants(none,[]),abstract_constants(none,[]),axioms(none,[]),theorems(none,[]),sets(none,[])])],[exporter_version(3)],_Error)).
+
diff --git a/sks/models/m0_3cars.eventb b/sks/models/m0_3cars.eventb
new file mode 100644
index 0000000..c9bdd88
--- /dev/null
+++ b/sks/models/m0_3cars.eventb
@@ -0,0 +1,2 @@
+package(load_event_b_project([event_b_model(none,m0_island_bridge,[sees(none,[context0]),variables(none,[identifier(none,n)]),invariant(none,[member(rodinpos(m0_island_bridge,inv1,internal_inv1I),identifier(none,n),natural_set(none)),less_equal(rodinpos(m0_island_bridge,inv2,internal_inv3I),identifier(none,n),identifier(none,d))]),theorems(none,[disjunct(rodinpos(m0_island_bridge,'DLF','_rtKkMHPmEeSdd99JEnI-rQ'),less(none,identifier(none,n),identifier(none,d)),greater(none,identifier(none,n),integer(none,0)))]),events(none,[event(rodinpos(m0_island_bridge,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos(m0_island_bridge,act1,internal_act1),[identifier(none,n)],[integer(none,0)])],[]),event(rodinpos(m0_island_bridge,'ML_out',internal_evt2),'ML_out',ordinary(none),[],[],[less(rodinpos(m0_island_bridge,grd1,internal_grd1),identifier(none,n),identifier(none,d))],[],[assign(rodinpos(m0_island_bridge,act1,internal_act1),[identifier(none,n)],[add(none,identifier(none,n),integer(none,1))])],[]),event(rodinpos(m0_island_bridge,'ML_in',internal_evt3),'ML_in',ordinary(none),[],[],[greater(rodinpos(m0_island_bridge,grd1,internal_grd1),identifier(none,n),integer(none,0))],[],[assign(rodinpos(m0_island_bridge,act1,internal_act1),[identifier(none,n)],[minus(none,identifier(none,n),integer(none,1))])],[])])])],[event_b_context(none,context0,[extends(none,[]),constants(none,[identifier(none,d),identifier(none,green),identifier(none,red)]),abstract_constants(none,[]),axioms(none,[conjunct(rodinpos(context0,axm1,internal_axm1A),member(none,identifier(none,d),natural1_set(none)),equal(none,identifier(none,d),integer(none,3))),equal(rodinpos(context0,axm2,internal_axm2A),identifier(none,'LIGHT'),set_extension(none,[identifier(none,green),identifier(none,red)])),not_equal(rodinpos(context0,axm3,internal_axm3A),identifier(none,green),identifier(none,red))]),theorems(none,[]),sets(none,[deferred_set(none,'LIGHT')])])],[exporter_version(3),po(m0_island_bridge,'Theorem',[invariant('DLF')],false),po(m0_island_bridge,'Invariant establishment',[event('INITIALISATION'),invariant(inv1)],true),po(m0_island_bridge,'Invariant establishment',[event('INITIALISATION'),invariant(inv2)],true),po(m0_island_bridge,'Invariant preservation',[event('ML_out'),invariant(inv1)],true),po(m0_island_bridge,'Invariant preservation',[event('ML_out'),invariant(inv2)],true),po(m0_island_bridge,'Invariant preservation',[event('ML_in'),invariant(inv1)],true),po(m0_island_bridge,'Invariant preservation',[event('ML_in'),invariant(inv2)],true)],_Error)).
+
diff --git a/sks/models/train_ctx0_beebook_ctx.eventb b/sks/models/train_ctx0_beebook_ctx.eventb
new file mode 100644
index 0000000..f9d17de
--- /dev/null
+++ b/sks/models/train_ctx0_beebook_ctx.eventb
@@ -0,0 +1,2 @@
+package(load_event_b_project([],[event_b_context(none,train_ctx0_beebook,[extends(none,[train_ctx0]),constants(none,[identifier(none,'A'),identifier(none,'B'),identifier(none,'C'),identifier(none,'D'),identifier(none,'E'),identifier(none,'F'),identifier(none,'G'),identifier(none,'H'),identifier(none,'I'),identifier(none,'J'),identifier(none,'K'),identifier(none,'L'),identifier(none,'M'),identifier(none,'N'),identifier(none,'R10'),identifier(none,'R1'),identifier(none,'R2'),identifier(none,'R3'),identifier(none,'R4'),identifier(none,'R5'),identifier(none,'R6'),identifier(none,'R7'),identifier(none,'R8'),identifier(none,'R9')]),abstract_constants(none,[]),axioms(none,[partition(rodinpos(train_ctx0_beebook,axm44,'_uj5LAIdoEeOcUOZ5WAG6MA'),identifier(none,'BLOCKS'),[set_extension(none,[identifier(none,'A')]),set_extension(none,[identifier(none,'B')]),set_extension(none,[identifier(none,'C')]),set_extension(none,[identifier(none,'D')]),set_extension(none,[identifier(none,'E')]),set_extension(none,[identifier(none,'F')]),set_extension(none,[identifier(none,'G')]),set_extension(none,[identifier(none,'H')]),set_extension(none,[identifier(none,'I')]),set_extension(none,[identifier(none,'J')]),set_extension(none,[identifier(none,'K')]),set_extension(none,[identifier(none,'L')]),set_extension(none,[identifier(none,'M')]),set_extension(none,[identifier(none,'N')])]),partition(rodinpos(train_ctx0_beebook,axm45,'_uj5LAYdoEeOcUOZ5WAG6MA'),identifier(none,'ROUTES'),[set_extension(none,[identifier(none,'R1')]),set_extension(none,[identifier(none,'R2')]),set_extension(none,[identifier(none,'R3')]),set_extension(none,[identifier(none,'R4')]),set_extension(none,[identifier(none,'R5')]),set_extension(none,[identifier(none,'R6')]),set_extension(none,[identifier(none,'R7')]),set_extension(none,[identifier(none,'R8')]),set_extension(none,[identifier(none,'R9')]),set_extension(none,[identifier(none,'R10')])]),equal(rodinpos(train_ctx0_beebook,compute_rtbl_from_nxt,'_tx3w0YdrEeOYLZrGGNvfWA'),identifier(none,rtbl),event_b_comprehension_set(none,[identifier(none,b),identifier(none,r)],couple(none,[identifier(none,b),identifier(none,r)]),conjunct(none,[member(none,identifier(none,b),identifier(none,'BLOCKS')),conjunct(none,[member(none,identifier(none,r),identifier(none,'ROUTES')),conjunct(none,[member(none,identifier(none,r),domain(none,identifier(none,nxt))),disjunct(none,member(none,identifier(none,b),domain(none,function(none,identifier(none,nxt),[identifier(none,r)]))),member(none,identifier(none,b),range(none,function(none,identifier(none,nxt),[identifier(none,r)]))))])])]))),equal(rodinpos(train_ctx0_beebook,axm40,'_uj5LA4doEeOcUOZ5WAG6MA'),identifier(none,nxt),set_extension(none,[couple(none,[identifier(none,'R1'),set_extension(none,[couple(none,[identifier(none,'L'),identifier(none,'A')]),couple(none,[identifier(none,'A'),identifier(none,'B')]),couple(none,[identifier(none,'B'),identifier(none,'C')])])]),couple(none,[identifier(none,'R2'),set_extension(none,[couple(none,[identifier(none,'L'),identifier(none,'A')]),couple(none,[identifier(none,'A'),identifier(none,'B')]),couple(none,[identifier(none,'B'),identifier(none,'D')]),couple(none,[identifier(none,'D'),identifier(none,'E')]),couple(none,[identifier(none,'E'),identifier(none,'F')]),couple(none,[identifier(none,'F'),identifier(none,'G')])])]),couple(none,[identifier(none,'R3'),set_extension(none,[couple(none,[identifier(none,'L'),identifier(none,'A')]),couple(none,[identifier(none,'A'),identifier(none,'B')]),couple(none,[identifier(none,'B'),identifier(none,'D')]),couple(none,[identifier(none,'D'),identifier(none,'K')]),couple(none,[identifier(none,'K'),identifier(none,'J')]),couple(none,[identifier(none,'J'),identifier(none,'N')])])]),couple(none,[identifier(none,'R4'),set_extension(none,[couple(none,[identifier(none,'M'),identifier(none,'H')]),couple(none,[identifier(none,'H'),identifier(none,'I')]),couple(none,[identifier(none,'I'),identifier(none,'K')]),couple(none,[identifier(none,'K'),identifier(none,'F')]),couple(none,[identifier(none,'F'),identifier(none,'G')])])]),couple(none,[identifier(none,'R5'),set_extension(none,[couple(none,[identifier(none,'M'),identifier(none,'H')]),couple(none,[identifier(none,'H'),identifier(none,'I')]),couple(none,[identifier(none,'I'),identifier(none,'J')]),couple(none,[identifier(none,'J'),identifier(none,'N')])])]),couple(none,[identifier(none,'R6'),set_extension(none,[couple(none,[identifier(none,'C'),identifier(none,'B')]),couple(none,[identifier(none,'B'),identifier(none,'A')]),couple(none,[identifier(none,'A'),identifier(none,'L')])])]),couple(none,[identifier(none,'R7'),set_extension(none,[couple(none,[identifier(none,'G'),identifier(none,'F')]),couple(none,[identifier(none,'F'),identifier(none,'E')]),couple(none,[identifier(none,'E'),identifier(none,'D')]),couple(none,[identifier(none,'D'),identifier(none,'B')]),couple(none,[identifier(none,'B'),identifier(none,'A')]),couple(none,[identifier(none,'A'),identifier(none,'L')])])]),couple(none,[identifier(none,'R8'),set_extension(none,[couple(none,[identifier(none,'N'),identifier(none,'J')]),couple(none,[identifier(none,'J'),identifier(none,'K')]),couple(none,[identifier(none,'K'),identifier(none,'D')]),couple(none,[identifier(none,'D'),identifier(none,'B')]),couple(none,[identifier(none,'B'),identifier(none,'A')]),couple(none,[identifier(none,'A'),identifier(none,'L')])])]),couple(none,[identifier(none,'R9'),set_extension(none,[couple(none,[identifier(none,'G'),identifier(none,'F')]),couple(none,[identifier(none,'F'),identifier(none,'K')]),couple(none,[identifier(none,'K'),identifier(none,'I')]),couple(none,[identifier(none,'I'),identifier(none,'H')]),couple(none,[identifier(none,'H'),identifier(none,'M')])])]),couple(none,[identifier(none,'R10'),set_extension(none,[couple(none,[identifier(none,'N'),identifier(none,'J')]),couple(none,[identifier(none,'J'),identifier(none,'I')]),couple(none,[identifier(none,'I'),identifier(none,'H')]),couple(none,[identifier(none,'H'),identifier(none,'M')])])])])),equal(rodinpos(train_ctx0_beebook,axm41,'_uj5LBIdoEeOcUOZ5WAG6MA'),identifier(none,fst),set_extension(none,[couple(none,[identifier(none,'R1'),identifier(none,'L')]),couple(none,[identifier(none,'R2'),identifier(none,'L')]),couple(none,[identifier(none,'R3'),identifier(none,'L')]),couple(none,[identifier(none,'R4'),identifier(none,'M')]),couple(none,[identifier(none,'R5'),identifier(none,'M')]),couple(none,[identifier(none,'R6'),identifier(none,'C')]),couple(none,[identifier(none,'R7'),identifier(none,'G')]),couple(none,[identifier(none,'R8'),identifier(none,'N')]),couple(none,[identifier(none,'R9'),identifier(none,'G')]),couple(none,[identifier(none,'R10'),identifier(none,'N')])])),equal(rodinpos(train_ctx0_beebook,axm42,'_uj5yEIdoEeOcUOZ5WAG6MA'),identifier(none,lst),set_extension(none,[couple(none,[identifier(none,'R1'),identifier(none,'C')]),couple(none,[identifier(none,'R2'),identifier(none,'G')]),couple(none,[identifier(none,'R3'),identifier(none,'N')]),couple(none,[identifier(none,'R4'),identifier(none,'G')]),couple(none,[identifier(none,'R5'),identifier(none,'N')]),couple(none,[identifier(none,'R6'),identifier(none,'L')]),couple(none,[identifier(none,'R7'),identifier(none,'L')]),couple(none,[identifier(none,'R8'),identifier(none,'L')]),couple(none,[identifier(none,'R9'),identifier(none,'M')]),couple(none,[identifier(none,'R10'),identifier(none,'M')])]))]),theorems(none,[]),sets(none,[])]),event_b_context(none,train_ctx0,[extends(none,[]),constants(none,[identifier(none,rtbl),identifier(none,lst),identifier(none,nxt),identifier(none,fst)]),abstract_constants(none,[]),axioms(none,[member(rodinpos(train_ctx0,axm1,internal_axm1A),identifier(none,rtbl),relations(none,identifier(none,'BLOCKS'),identifier(none,'ROUTES'))),equal(rodinpos(train_ctx0,axm2,internal_axm2A),domain(none,identifier(none,rtbl)),identifier(none,'BLOCKS')),equal(rodinpos(train_ctx0,axm3,internal_axm3A),range(none,identifier(none,rtbl)),identifier(none,'ROUTES')),member(rodinpos(train_ctx0,axm4,internal_axm4A),identifier(none,nxt),total_function(none,identifier(none,'ROUTES'),partial_injection(none,identifier(none,'BLOCKS'),identifier(none,'BLOCKS')))),member(rodinpos(train_ctx0,axm5,internal_axm5A),identifier(none,fst),total_function(none,identifier(none,'ROUTES'),identifier(none,'BLOCKS'))),member(rodinpos(train_ctx0,axm6,internal_axm6A),identifier(none,lst),total_function(none,identifier(none,'ROUTES'),identifier(none,'BLOCKS'))),subset(rodinpos(train_ctx0,axm7,internal_axm7A),reverse(none,identifier(none,fst)),identifier(none,rtbl)),subset(rodinpos(train_ctx0,axm8,internal_axm8A),reverse(none,identifier(none,lst)),identifier(none,rtbl)),forall(rodinpos(train_ctx0,axm11,internal_axm11A),[identifier(none,r)],implication(none,conjunct(none,[member(none,identifier(none,r),identifier(none,'ROUTES')),member(none,identifier(none,r),identifier(none,'ROUTES'))]),not_equal(none,function(none,identifier(none,fst),[identifier(none,r)]),function(none,identifier(none,lst),[identifier(none,r)])))),forall(rodinpos(train_ctx0,axm10,internal_axm10A),[identifier(none,r)],implication(none,conjunct(none,[member(none,identifier(none,r),identifier(none,'ROUTES')),member(none,identifier(none,r),identifier(none,'ROUTES'))]),forall(none,[identifier(none,'S')],implication(none,conjunct(none,[member(none,identifier(none,'S'),pow_subset(none,identifier(none,'BLOCKS'))),conjunct(none,[subset(none,identifier(none,'S'),range(none,function(none,identifier(none,nxt),[identifier(none,r)]))),subset(none,identifier(none,'S'),image(none,function(none,identifier(none,nxt),[identifier(none,r)]),identifier(none,'S')))])]),equal(none,identifier(none,'S'),typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))))))),forall(rodinpos(train_ctx0,axm9,internal_axm9A),[identifier(none,r)],implication(none,conjunct(none,[member(none,identifier(none,r),identifier(none,'ROUTES')),member(none,identifier(none,r),identifier(none,'ROUTES'))]),member(none,function(none,identifier(none,nxt),[identifier(none,r)]),total_bijection(none,set_subtraction(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])),set_extension(none,[function(none,identifier(none,lst),[identifier(none,r)])])),set_subtraction(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])),set_extension(none,[function(none,identifier(none,fst),[identifier(none,r)])])))))),forall(rodinpos(train_ctx0,axm12,internal_axm12A),[identifier(none,r),identifier(none,s)],implication(none,conjunct(none,[member(none,identifier(none,r),identifier(none,'ROUTES')),conjunct(none,[member(none,identifier(none,s),identifier(none,'ROUTES')),conjunct(none,[member(none,identifier(none,r),identifier(none,'ROUTES')),conjunct(none,[member(none,identifier(none,s),identifier(none,'ROUTES')),not_equal(none,identifier(none,r),identifier(none,s))])])])]),not_member(none,function(none,identifier(none,fst),[identifier(none,r)]),set_subtraction(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,s)])),set_extension(none,[function(none,identifier(none,fst),[identifier(none,s)]),function(none,identifier(none,lst),[identifier(none,s)])]))))),forall(rodinpos(train_ctx0,axm13,internal_axm13A),[identifier(none,r),identifier(none,s)],implication(none,conjunct(none,[member(none,identifier(none,r),identifier(none,'ROUTES')),conjunct(none,[member(none,identifier(none,s),identifier(none,'ROUTES')),conjunct(none,[member(none,identifier(none,r),identifier(none,'ROUTES')),conjunct(none,[member(none,identifier(none,s),identifier(none,'ROUTES')),not_equal(none,identifier(none,r),identifier(none,s))])])])]),not_member(none,function(none,identifier(none,lst),[identifier(none,r)]),set_subtraction(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,s)])),set_extension(none,[function(none,identifier(none,fst),[identifier(none,s)]),function(none,identifier(none,lst),[identifier(none,s)])])))))]),theorems(none,[]),sets(none,[deferred_set(none,'ROUTES'),deferred_set(none,'BLOCKS')])])],[exporter_version(3),po(train_ctx0_beebook,'Well-definedness of Axiom',[axiom(compute_rtbl_from_nxt)],false),po(train_ctx0,'Well-definedness of Axiom',[axiom(axm11)],true),po(train_ctx0,'Well-definedness of Axiom',[axiom(axm10)],true),po(train_ctx0,'Well-definedness of Axiom',[axiom(axm9)],true),po(train_ctx0,'Well-definedness of Axiom',[axiom(axm12)],true),po(train_ctx0,'Well-definedness of Axiom',[axiom(axm13)],true)],_Error)).
+
--
GitLab