Skip to content
Snippets Groups Projects
Commit 9ed38dfc authored by Michael Leuschel's avatar Michael Leuschel
Browse files

add Rodin Real example 


Signed-off-by: default avatarMichael Leuschel <leuschel@uni-duesseldorf.de>
parent 6922100e
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Physics/SpringPhysics_prob01_mch.eventb 0 → 100644
+ 2
− 0
View file @ 9ed38dfc
package(load_event_b_project([event_b_model(none,'SpringPhysics_prob01',[sees(none,['SpringConstants']),refines(none,'SpringPhysics'),variables(none,[identifier(none,dist),identifier(none,speed)]),invariant(none,[]),theorems(none,[]),events(none,[event(rodinpos('SpringPhysics_prob01','INITIALISATION',','),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('SpringPhysics_prob01',act1,'\''),[identifier(none,dist)],[typeof(none,extended_expr(none,one,[],[]),extended_expr(none,'\20435\',[],[]))]),assign(rodinpos('SpringPhysics_prob01',act2,'('),[identifier(none,speed)],[typeof(none,extended_expr(none,zero,[],[]),extended_expr(none,'\20435\',[],[]))])],[]),event(rodinpos('SpringPhysics_prob01',move_spring,'-'),move_spring,ordinary(none),[move_spring],[identifier(rodinpos('SpringPhysics_prob01',[],'-'),acc),identifier(rodinpos('SpringPhysics_prob01',[],'\''),delta)],[truth(rodinpos('SpringPhysics_prob01','smr(delta,one)','(')),truth(rodinpos('SpringPhysics_prob01','smr(zero,delta)',')')),member(rodinpos('SpringPhysics_prob01',grd1,'+'),identifier(none,delta),typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),member(rodinpos('SpringPhysics_prob01',grd2,'.'),identifier(none,acc),typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),equal(rodinpos('SpringPhysics_prob01',grd3,'/'),identifier(none,acc),typeof(none,extended_expr(none,mult,[typeof(none,extended_expr(none,minus,[identifier(none,dist)],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,inv,[identifier(none,mass)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))),equal(rodinpos('SpringPhysics_prob01',grd4,'('),identifier(none,delta),typeof(none,extended_expr(none,inv,[typeof(none,extended_expr(none,mult,[identifier(none,four),identifier(none,four)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[])))],[],[assign(rodinpos('SpringPhysics_prob01',act1,'*'),[identifier(none,dist)],[typeof(none,extended_expr(none,plus,[identifier(none,dist),typeof(none,extended_expr(none,mult,[identifier(none,speed),typeof(none,extended_expr(none,inv,[identifier(none,delta)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))]),assign(rodinpos('SpringPhysics_prob01',act2,','),[identifier(none,speed)],[typeof(none,extended_expr(none,plus,[identifier(none,speed),typeof(none,extended_expr(none,mult,[identifier(none,acc),typeof(none,extended_expr(none,inv,[identifier(none,delta)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))])],[])])]),event_b_model(none,'SpringPhysics',[sees(none,['SpringConstants']),variables(none,[identifier(none,dist),identifier(none,speed)]),invariant(none,[member(rodinpos('SpringPhysics',inv1,')'),identifier(none,dist),typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),member(rodinpos('SpringPhysics',inv2,','),identifier(none,speed),typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))))]),theorems(none,[]),events(none,[event(rodinpos('SpringPhysics','INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('SpringPhysics',act1,'\''),[identifier(none,dist)],[typeof(none,extended_expr(none,one,[],[]),extended_expr(none,'\20435\',[],[]))]),assign(rodinpos('SpringPhysics',act2,'('),[identifier(none,speed)],[typeof(none,extended_expr(none,zero,[],[]),extended_expr(none,'\20435\',[],[]))])],[]),event(rodinpos('SpringPhysics',move_spring,'*'),move_spring,ordinary(none),[],[identifier(rodinpos('SpringPhysics',[],'-'),acc),identifier(rodinpos('SpringPhysics',[],'\''),delta)],[truth(rodinpos('SpringPhysics','smr(delta,one)','(')),truth(rodinpos('SpringPhysics','smr(zero,delta)',')')),member(rodinpos('SpringPhysics',grd1,'+'),identifier(none,delta),typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),member(rodinpos('SpringPhysics',grd2,'.'),identifier(none,acc),typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),equal(rodinpos('SpringPhysics',grd3,'/'),identifier(none,acc),typeof(none,extended_expr(none,mult,[typeof(none,extended_expr(none,minus,[identifier(none,dist)],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,inv,[identifier(none,mass)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[])))],[],[assign(rodinpos('SpringPhysics',act1,'*'),[identifier(none,dist)],[typeof(none,extended_expr(none,plus,[identifier(none,dist),typeof(none,extended_expr(none,mult,[identifier(none,speed),typeof(none,extended_expr(none,inv,[identifier(none,delta)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))]),assign(rodinpos('SpringPhysics',act2,','),[identifier(none,speed)],[typeof(none,extended_expr(none,plus,[identifier(none,speed),typeof(none,extended_expr(none,mult,[identifier(none,acc),typeof(none,extended_expr(none,inv,[identifier(none,delta)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))])],[])])])],[event_b_context(none,'SpringConstants',[extends(none,[]),constants(none,[identifier(none,sixteen),identifier(none,four),identifier(none,mass)]),abstract_constants(none,[]),axioms(none,[member(rodinpos('SpringConstants',axm1,'('),identifier(none,mass),typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),equal(rodinpos('SpringConstants',axm2,')'),identifier(none,four),typeof(none,extended_expr(none,plus,[typeof(none,extended_expr(none,plus,[typeof(none,extended_expr(none,one,[],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,one,[],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,plus,[typeof(none,extended_expr(none,one,[],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,one,[],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))),member(rodinpos('SpringConstants',axm3,'+'),identifier(none,four),typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),equal(rodinpos('SpringConstants',axm4,','),identifier(none,sixteen),typeof(none,extended_expr(none,mult,[typeof(none,extended_expr(none,mult,[identifier(none,four),identifier(none,four)],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,mult,[identifier(none,four),identifier(none,four)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))),member(rodinpos('SpringConstants',axm5,'.'),identifier(none,sixteen),typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),equal(rodinpos('SpringConstants',axm6,'/'),identifier(none,mass),typeof(none,extended_expr(none,mult,[identifier(none,sixteen),identifier(none,sixteen)],[]),extended_expr(none,'\20435\',[],[])))]),theorems(none,[]),sets(none,[])])],[exporter_version(3),po('SpringPhysics_prob01','Well-definedness of Guard',[guard(grd4),event(move_spring)],false),po('SpringPhysics','Well-definedness of Guard',[guard(grd3),event(move_spring)],false),po('SpringPhysics','Well-definedness of action',[action(act1)],false),po('SpringPhysics','Well-definedness of action',[action(act2)],false),theory(theory_name('RealTheory2','Real2'),[],[],[],[],[axiomatic_def_block(real_def,['\20435\'],[opdef(plus,[argument(a,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),argument(b,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))))],[]),opdef(zero,[],[]),opdef(minus,[argument(a,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))))],[]),opdef(mult,[argument(a,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),argument(b,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))))],[]),opdef(one,[],[]),opdef(inv,[argument(a,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))))],[]),opdef(leq,[argument(a,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),argument(b,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))))],[]),opdef(sup,[argument('A',pow_subset(none,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))))],[]),opdef(inf,[argument('A',pow_subset(none,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))))],[]),opdef(smr,[argument(a,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),argument(b,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))))],[]),opdef(sub,[argument(a,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),argument(b,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))))],[]),opdef(cnt,[argument(f,pow_subset(none,cartesian_product(none,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))),typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))))),argument(x,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))))],[]),opdef(gtr,[argument(a,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[])))),argument(b,typeof(none,extended_expr(none,'\20435\',[],[]),pow_subset(none,extended_expr(none,'\20435\',[],[]))))],[])],[forall(none,[identifier(none,x),identifier(none,y)],implication(none,conjunct(none,[member(none,identifier(none,x),extended_expr(none,'\20435\',[],[])),member(none,identifier(none,y),extended_expr(none,'\20435\',[],[]))]),equal(none,typeof(none,extended_expr(none,plus,[identifier(none,x),identifier(none,y)],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,plus,[identifier(none,y),identifier(none,x)],[]),extended_expr(none,'\20435\',[],[]))))),forall(none,[identifier(none,x),identifier(none,y),identifier(none,z)],implication(none,conjunct(none,[member(none,identifier(none,x),extended_expr(none,'\20435\',[],[])),conjunct(none,[member(none,identifier(none,y),extended_expr(none,'\20435\',[],[])),member(none,identifier(none,z),extended_expr(none,'\20435\',[],[]))])]),equal(none,typeof(none,extended_expr(none,plus,[typeof(none,extended_expr(none,plus,[identifier(none,x),identifier(none,y)],[]),extended_expr(none,'\20435\',[],[])),identifier(none,z)],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,plus,[identifier(none,x),typeof(none,extended_expr(none,plus,[identifier(none,y),identifier(none,z)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))))),forall(none,[identifier(none,x)],implication(none,member(none,identifier(none,x),extended_expr(none,'\20435\',[],[])),equal(none,typeof(none,extended_expr(none,plus,[identifier(none,x),typeof(none,extended_expr(none,zero,[],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[])),identifier(none,x)))),forall(none,[identifier(none,x)],implication(none,member(none,identifier(none,x),extended_expr(none,'\20435\',[],[])),equal(none,typeof(none,extended_expr(none,plus,[identifier(none,x),typeof(none,extended_expr(none,minus,[identifier(none,x)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,zero,[],[]),extended_expr(none,'\20435\',[],[]))))),forall(none,[identifier(none,x),identifier(none,y)],implication(none,conjunct(none,[member(none,identifier(none,x),extended_expr(none,'\20435\',[],[])),member(none,identifier(none,y),extended_expr(none,'\20435\',[],[]))]),equal(none,typeof(none,extended_expr(none,mult,[identifier(none,x),identifier(none,y)],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,mult,[identifier(none,y),identifier(none,x)],[]),extended_expr(none,'\20435\',[],[]))))),forall(none,[identifier(none,x),identifier(none,y),identifier(none,z)],implication(none,conjunct(none,[member(none,identifier(none,x),extended_expr(none,'\20435\',[],[])),conjunct(none,[member(none,identifier(none,y),extended_expr(none,'\20435\',[],[])),member(none,identifier(none,z),extended_expr(none,'\20435\',[],[]))])]),equal(none,typeof(none,extended_expr(none,mult,[typeof(none,extended_expr(none,mult,[identifier(none,x),identifier(none,y)],[]),extended_expr(none,'\20435\',[],[])),identifier(none,z)],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,mult,[identifier(none,x),typeof(none,extended_expr(none,mult,[identifier(none,y),identifier(none,z)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[]))))),forall(none,[identifier(none,x)],implication(none,member(none,identifier(none,x),extended_expr(none,'\20435\',[],[])),equal(none,typeof(none,extended_expr(none,mult,[identifier(none,x),typeof(none,extended_expr(none,one,[],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[])),identifier(none,x)))),forall(none,[identifier(none,x)],implication(none,conjunct(none,[member(none,identifier(none,x),extended_expr(none,'\20435\',[],[])),not_equal(none,identifier(none,x),typeof(none,extended_expr(none,zero,[],[]),extended_expr(none,'\20435\',[],[])))]),equal(none,typeof(none,extended_expr(none,mult,[identifier(none,x),typeof(none,extended_expr(none,inv,[identifier(none,x)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,one,[],[]),extended_expr(none,'\20435\',[],[]))))),not_equal(none,typeof(none,extended_expr(none,zero,[],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,one,[],[]),extended_expr(none,'\20435\',[],[]))),forall(none,[identifier(none,x),identifier(none,y),identifier(none,z)],implication(none,conjunct(none,[member(none,identifier(none,x),extended_expr(none,'\20435\',[],[])),conjunct(none,[member(none,identifier(none,y),extended_expr(none,'\20435\',[],[])),member(none,identifier(none,z),extended_expr(none,'\20435\',[],[]))])]),equal(none,typeof(none,extended_expr(none,mult,[identifier(none,x),typeof(none,extended_expr(none,plus,[identifier(none,y),identifier(none,z)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,plus,[typeof(none,extended_expr(none,mult,[identifier(none,x),identifier(none,y)],[]),extended_expr(none,'\20435\',[],[])),typeof(none,extended_expr(none,mult,[identifier(none,x),identifier(none,z)],[]),extended_expr(none,'\20435\',[],[]))],[]),extended_expr(none,'\20435\',[],[])))))])],[])],_Error)).
Physics/spring_physics.json 0 → 100644
+ 31
− 0
View file @ 9ed38dfc
{
"svg": "spring_physics.svg",
"comment": "version which uses new svg object creation",
"items": [
{
"id": "body0",
"attr": "cx",
"value" : "dist * 100.0"
},
{
"id": "speed0",
"attr": "x1",
"value" : "dist * 100.0"
},
{
"id": "speed0",
"attr": "x2",
"value" : "(dist+speed*100.0) * 100.0"
}
],
"events": [
{
"id": "body0",
"event": "move_spring",
"hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"},
{ "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
}
]
}
Physics/spring_physics.svg 0 → 100644
+ 44
− 0
View file @ 9ed38dfc
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<svg
xmlns="http://www.w3.org/2000/svg"
height="100" width="400"
viewBox="-140 -15 280 30"
>
<defs>
<marker id="arrowhead" markerWidth="10" markerHeight="7"
refX="0" refY="3.5" orient="auto">
<polygon points="0 0, 10 3.5, 0 7" />
</marker>
<marker id="startarrow" markerWidth="10" markerHeight="7"
refX="10" refY="3.5" orient="auto">
<polygon points="10 0, 10 7, 0 3.5" fill="green" />
</marker>
<marker id="endarrow" markerWidth="10" markerHeight="7"
refX="0" refY="3.5" orient="auto">
<polygon points="0 0, 10 3.5, 0 7" fill="green" />
</marker>
</defs>
<circle id="body0" cx="45" cy="0" r="9.5"
stroke="black" stroke-width="0.5" fill="wheat" />
<line x1="45" y1="0" x2="55" y2="0" stroke="#000"
stroke-width="0.5" marker-end="url(#arrowhead)"
id = "speed0"
/>
<line x1="0" y1="-10" x2="0" y2="10" stroke="gray"
stroke-width="0.5"
/>
<line x1="100" y1="-5" x2="100" y2="5" stroke="gray"
stroke-width="0.5"
/>
<line x1="-100" y1="-5" x2="-100" y2="5" stroke="gray"
stroke-width="0.5"
/>
</svg>
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment