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.

272 lines
11 KiB

6 years ago
<?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="78.256187mm"
height="41.567307mm"
viewBox="0 0 277.2857 147.28573"
id="svg2"
version="1.1"
inkscape:version="0.91 r13725"
sodipodi:docname="Function2_1.svg">
<defs
id="defs4">
<marker
inkscape:stockid="Arrow2Lend"
orient="auto"
refY="0"
refX="0"
id="marker4597"
style="overflow:visible"
inkscape:isstock="true">
<path
id="path4599"
style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
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"
transform="matrix(-1.1,0,0,-1.1,-1.1,0)"
inkscape:connector-curvature="0" />
</marker>
<marker
inkscape:isstock="true"
style="overflow:visible"
id="marker4561"
refX="0"
refY="0"
orient="auto"
inkscape:stockid="Arrow1Lend">
<path
transform="matrix(-0.8,0,0,-0.8,-10,0)"
style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1"
d="M 0,0 5,-5 -12.5,0 5,5 0,0 Z"
id="path4563"
inkscape:connector-curvature="0" />
</marker>
<marker
inkscape:isstock="true"
style="overflow:visible"
id="marker4501"
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"
inkscape:connector-curvature="0" />
</marker>
<marker
inkscape:isstock="true"
style="overflow:visible"
id="marker4441"
refX="0"
refY="0"
orient="auto"
inkscape:stockid="Arrow1Lend">
<path
transform="matrix(-0.8,0,0,-0.8,-10,0)"
style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1"
d="M 0,0 5,-5 -12.5,0 5,5 0,0 Z"
id="path4443"
inkscape:connector-curvature="0" />
</marker>
<marker
inkscape:isstock="true"
style="overflow:visible"
id="marker4501-0"
refX="0"
refY="0"
orient="auto"
inkscape:stockid="Arrow2Lend"
inkscape:collect="always">
<path
inkscape:connector-curvature="0"
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-9" />
</marker>
<marker
inkscape:isstock="true"
style="overflow:visible"
id="marker4501-6"
refX="0"
refY="0"
orient="auto"
inkscape:stockid="Arrow2Lend"
inkscape:collect="always">
<path
inkscape:connector-curvature="0"
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-2" />
</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="-579.41219"
inkscape:cy="355.43353"
inkscape:document-units="px"
inkscape:current-layer="layer2"
showgrid="true"
showborder="false"
fit-margin-top="0"
fit-margin-left="0"
fit-margin-right="0"
fit-margin-bottom="0"
inkscape:window-width="1920"
inkscape:window-height="1018"
inkscape:window-x="1713"
inkscape:window-y="72"
inkscape:window-maximized="0">
<inkscape:grid
type="xygrid"
id="grid4155"
originx="-111.35713"
originy="-691.3572" />
</sodipodi:namedview>
<metadata
id="metadata7">
<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(-111.35714,-213.71933)"
style="display:inline">
<rect
style="fill:none;fill-opacity:1;stroke:#000000;stroke-width:2.24441051;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
id="rect4136"
width="125.66988"
height="89.241302"
x="190.0222"
y="242.3844" />
<circle
style="fill:#00a02b;fill-opacity:1;stroke:none;stroke-width:2.20000005;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
id="path4159"
cx="253.9137"
cy="287.48911"
r="12.5" />
<g
id="g5678">
<path
sodipodi:nodetypes="ccc"
inkscape:connector-curvature="0"
id="path4138"
d="m 127.99999,261.93363 48.29193,0 10.99379,0"
style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1.29999995;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:3.4000001;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker4501)" />
<path
inkscape:connector-curvature="0"
id="path5533"
d="m 125.15944,261.79585 60,0 0,0"
style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:3;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4.4000001;stroke-dasharray:none;stroke-opacity:1" />
</g>
<g
transform="translate(0,50.000003)"
id="g5678-3">
<path
sodipodi:nodetypes="ccc"
inkscape:connector-curvature="0"
id="path4138-6"
d="m 127.99999,261.93363 48.29193,0 10.99379,0"
style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1.29999995;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:3.4000001;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker4501-0)" />
<path
inkscape:connector-curvature="0"
id="path5533-0"
d="m 125.15944,261.79585 60,0 0,0"
style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:3;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4.4000001;stroke-dasharray:none;stroke-opacity:1" />
</g>
<g
transform="translate(190.71429,25.000003)"
id="g5678-6">
<path
sodipodi:nodetypes="ccc"
inkscape:connector-curvature="0"
id="path4138-1"
d="m 127.99999,261.93363 48.29193,0 10.99379,0"
style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1.29999995;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:3.4000001;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker4501-6)" />
<path
inkscape:connector-curvature="0"
id="path5533-8"
d="m 125.15944,261.79585 60,0 0,0"
style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:3;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4.4000001;stroke-dasharray:none;stroke-opacity:1" />
</g>
<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="122.85715"
y="253.07648"
id="text5843"
sodipodi:linespacing="125%"><tspan
sodipodi:role="line"
id="tspan5845"
x="122.85715"
y="253.07648"
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">I1</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="122.75949"
y="352.36218"
id="text5843-5"
sodipodi:linespacing="125%"><tspan
sodipodi:role="line"
id="tspan5845-0"
x="122.75949"
y="352.36218"
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">I2</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="337.85715"
y="277.36218"
id="text5843-2"
sodipodi:linespacing="125%"><tspan
sodipodi:role="line"
id="tspan5845-9"
x="337.85715"
y="277.36218"
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">O</tspan></text>
</g>
<g
inkscape:groupmode="layer"
id="layer2"
inkscape:label="contour"
style="display:none"
transform="translate(3.5120392e-6,3.2654572e-6)">
<rect
transform="translate(-111.35714,-213.71933)"
style="display:inline;fill:none;fill-opacity:1;stroke:#00e100;stroke-width:1.90964365;stroke-miterlimit:4.4000001;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
id="rect5873"
width="275.37607"
height="145.37608"
x="112.31196"
y="214.67415" />
</g>
</svg>