This project is a demonstrator tool, made by the MOISE project, that translates timed Altarica models into Fiacre models. Such translation allows to use model checkers such as Tina to prove properties. The project contains the translator tool.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 
 
 
 

276 lines
12 KiB

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!-- Created with Inkscape (http://www.inkscape.org/) -->
<svg
xmlns:dc="http://purl.org/dc/elements/1.1/"
xmlns:cc="http://creativecommons.org/ns#"
xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
xmlns:svg="http://www.w3.org/2000/svg"
xmlns="http://www.w3.org/2000/svg"
xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
width="176.10666mm"
height="91.036827mm"
viewBox="0 0 623.99997 322.57143"
id="svg4267"
version="1.1"
inkscape:version="0.91 r13725"
sodipodi:docname="Function2_2.svg">
<defs
id="defs4269">
<marker
inkscape:stockid="Arrow1Lend"
orient="auto"
refY="0"
refX="0"
id="Arrow1Lend"
style="overflow:visible"
inkscape:isstock="true">
<path
id="path5474"
d="M 0,0 5,-5 -12.5,0 5,5 0,0 Z"
style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1"
transform="matrix(-0.8,0,0,-0.8,-10,0)"
inkscape:connector-curvature="0" />
</marker>
<marker
inkscape:isstock="true"
style="overflow:visible"
id="marker4501-3"
refX="0"
refY="0"
orient="auto"
inkscape:stockid="Arrow2Lend"
inkscape:collect="always">
<path
transform="matrix(-1.1,0,0,-1.1,-1.1,0)"
d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
id="path4503-6"
inkscape:connector-curvature="0" />
</marker>
<marker
inkscape:isstock="true"
style="overflow:visible"
id="marker4501-3-2"
refX="0"
refY="0"
orient="auto"
inkscape:stockid="Arrow2Lend"
inkscape:collect="always">
<path
transform="matrix(-1.1,0,0,-1.1,-1.1,0)"
d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
id="path4503-6-6"
inkscape:connector-curvature="0" />
</marker>
<marker
inkscape:isstock="true"
style="overflow:visible"
id="marker4501-3-2-8"
refX="0"
refY="0"
orient="auto"
inkscape:stockid="Arrow2Lend"
inkscape:collect="always">
<path
transform="matrix(-1.1,0,0,-1.1,-1.1,0)"
d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
id="path4503-6-6-7"
inkscape:connector-curvature="0" />
</marker>
<marker
inkscape:isstock="true"
style="overflow:visible"
id="marker4501-3-2-2"
refX="0"
refY="0"
orient="auto"
inkscape:stockid="Arrow2Lend"
inkscape:collect="always">
<path
transform="matrix(-1.1,0,0,-1.1,-1.1,0)"
d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
id="path4503-6-6-0"
inkscape:connector-curvature="0" />
</marker>
</defs>
<sodipodi:namedview
id="base"
pagecolor="#ffffff"
bordercolor="#666666"
borderopacity="1.0"
inkscape:pageopacity="0.0"
inkscape:pageshadow="2"
inkscape:zoom="0.7"
inkscape:cx="242.03107"
inkscape:cy="8.0838619"
inkscape:document-units="px"
inkscape:current-layer="layer3"
showgrid="true"
fit-margin-top="0"
fit-margin-left="0"
fit-margin-right="0"
fit-margin-bottom="0"
inkscape:window-width="1271"
inkscape:window-height="715"
inkscape:window-x="1813"
inkscape:window-y="172"
inkscape:window-maximized="0">
<inkscape:grid
type="xygrid"
id="grid4815"
originx="10.571428"
originy="-583.71426" />
</sodipodi:namedview>
<metadata
id="metadata4272">
<rdf:RDF>
<cc:Work
rdf:about="">
<dc:format>image/svg+xml</dc:format>
<dc:type
rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
<dc:title></dc:title>
</cc:Work>
</rdf:RDF>
</metadata>
<g
inkscape:label="Calque 1"
inkscape:groupmode="layer"
id="layer1"
transform="translate(10.571429,-146.07647)">
<rect
style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:3;stroke-linejoin:round;stroke-miterlimit:4.4000001;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
id="rect4817"
width="200"
height="80"
x="80"
y="232.3622" />
<ellipse
style="fill:#000000;fill-opacity:1;stroke:#000000;stroke-width:3.47510362;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
id="path5787"
cx="12.142852"
cy="167.22244"
rx="13.705303"
ry="12.13697" />
<rect
style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:3;stroke-linejoin:round;stroke-miterlimit:4.4000001;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
id="rect4817-5"
width="200"
height="80"
x="401.42856"
y="230.93362" />
<rect
style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:3;stroke-linejoin:round;stroke-miterlimit:4.4000001;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
id="rect4817-6"
width="200"
height="80"
x="400"
y="378.7193" />
<path
style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:4;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
d="m 20,172.3622 c 60,60 60,60 60,60"
id="path6043"
inkscape:connector-curvature="0" />
<path
style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:4;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
d="m 280,272.3622 115.64372,-0.25254"
id="path6045"
inkscape:connector-curvature="0"
sodipodi:nodetypes="cc" />
<path
style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:4;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
d="m 499.16317,377.23966 0.47969,-52.55603"
id="path6047"
inkscape:connector-curvature="0"
sodipodi:nodetypes="cc" />
<path
style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:4;stroke-linecap:butt;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
d="m 281.42857,272.3622 c 0,0 19.10499,0.0429 23.98878,14.25396 8.95709,26.06364 14.58265,70.74604 22.17048,86.35494 12.10522,24.90162 67.94788,23.67681 67.94788,23.67681"
id="path6049"
inkscape:connector-curvature="0"
inkscape:transform-center-x="-7.1428571"
inkscape:transform-center-y="-28.571429"
sodipodi:nodetypes="cssc" />
<path
style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2.13773298;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:3.4000001;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker4501-3)"
d="m 66.912762,219.37924 12.310717,12.07092"
id="path4138-5"
inkscape:connector-curvature="0"
sodipodi:nodetypes="cc" />
<path
style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2.13773298;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:3.4000001;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker4501-3-2)"
d="m 381.63992,272.65885 17.24073,-0.13505"
id="path4138-5-1"
inkscape:connector-curvature="0"
sodipodi:nodetypes="cc" />
<path
style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2.13773298;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:3.4000001;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker4501-3-2-8)"
d="m 379.22921,396.58742 17.24073,-0.13505"
id="path4138-5-1-9"
inkscape:connector-curvature="0"
sodipodi:nodetypes="cc" />
<path
style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2.13773298;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:3.4000001;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker4501-3-2-2)"
d="m 499.73482,330.21872 -0.24887,-17.23946"
id="path4138-5-1-2"
inkscape:connector-curvature="0"
sodipodi:nodetypes="cc" />
<text
xml:space="preserve"
style="font-style:normal;font-weight:normal;font-size:40px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
x="111.14286"
y="280.93365"
id="text8261"
sodipodi:linespacing="125%"><tspan
sodipodi:role="line"
id="tspan8263"
x="111.14286"
y="280.93365"
style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:40px;line-height:125%;font-family:'Liberation Serif';-inkscape-font-specification:'Liberation Serif, Normal';text-align:start;writing-mode:lr-tb;text-anchor:start">nominal</tspan></text>
<text
xml:space="preserve"
style="font-style:normal;font-weight:normal;font-size:40px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
x="447.14285"
y="280.93365"
id="text8261-4"
sodipodi:linespacing="125%"><tspan
sodipodi:role="line"
id="tspan8263-2"
x="447.14285"
y="280.93365"
style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:40px;line-height:125%;font-family:'Liberation Serif';-inkscape-font-specification:'Liberation Serif, Normal';text-align:start;writing-mode:lr-tb;text-anchor:start">lost</tspan></text>
<text
xml:space="preserve"
style="font-style:normal;font-weight:normal;font-size:40px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
x="423.14285"
y="428.07651"
id="text8261-9"
sodipodi:linespacing="125%"
inkscape:transform-center-x="-8.5714289"
inkscape:transform-center-y="-4.285714"><tspan
sodipodi:role="line"
id="tspan8263-6"
x="423.14285"
y="428.07651"
style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:40px;line-height:125%;font-family:'Liberation Serif';-inkscape-font-specification:'Liberation Serif, Normal';text-align:start;writing-mode:lr-tb;text-anchor:start">erroneous</tspan></text>
</g>
<g
inkscape:groupmode="layer"
id="layer3"
inkscape:label="contour"
transform="translate(10.571429,-146.07647)"
style="display:none">
<rect
style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:3.75491953;stroke-linejoin:round;stroke-miterlimit:4;stroke-dasharray:3.7549195, 7.509839;stroke-dashoffset:0;stroke-opacity:1"
id="rect8292"
width="620.24506"
height="318.81653"
x="-8.6939688"
y="147.95393" />
</g>
</svg>