Skip to content
Snippets Groups Projects
Commit bb505aad authored by Alberto Debiasi's avatar Alberto Debiasi
Browse files

Implement tests for basic operations. 

Change-Id: Id2f57b35fe17473afa047a42718ef712ba8e82c0
parent ba9d0f90
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 4871 additions and 3 deletions
plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/META-INF/MANIFEST.MF
+ 13
− 2
View file @ bb505aad
...@@ -26,6 +26,17 @@ Require-Bundle: eu.fbk.eclipse.standardtools.utils, ...@@ -26,6 +26,17 @@ Require-Bundle: eu.fbk.eclipse.standardtools.utils,
eu.fbk.tools.editor.oss, eu.fbk.tools.editor.oss,
eu.fbk.eclipse.standardtools.xtextService, eu.fbk.eclipse.standardtools.xtextService,
org.eclipse.xtext, org.eclipse.xtext,
eu.fbk.tools.adapter.core eu.fbk.tools.adapter.core,
org.eclipse.papyrus.junit.framework,
org.eclipse.papyrus.junit.utils,
eu.fbk.eclipse.standardtools.StateMachineTranslatorToSmv,
eu.fbk.eclipse.standardtools.ExecOcraCommands,
eu.fbk.eclipse.standardtools.diagram.ui,
eu.fbk.eclipse.standardtools.diagram,
org.polarsys.chess.diagram.ui,
eu.fbk.tools.adapter.ui
Bundle-ActivationPolicy: lazy Bundle-ActivationPolicy: lazy
Import-Package: org.apache.log4j Import-Package: eu.fbk.eclipse.standardtools.logger,
eu.fbk.tools.adapter.ui.preferences,
org.apache.commons.io,
org.apache.log4j
plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/configTest.properties
+ 5
− 1
View file @ bb505aad
OCRAPath=C:\\Users\\Alberto\\Downloads\\20180124_OpenCertCHESSClient_Win_x64\\amass_P1\\FBK_Tools\\OCRA\\ocra_win64.exe OCRAPath=C:\\Users\\Alberto\\Downloads\\20180124_OpenCertCHESSClient_Win_x64\\amass_P1\\FBK_Tools\\OCRA\\ocra_win64.exe
workspace=C:\\Windows\\Temp\\amass\\ testOutput=testOutput
\ No newline at end of file testTempOutput=testTempOutput
OCRAFilePath=resources\\tools\\ocra_win64.exe
nuXmvFilePath=resources\\tools\\nuXmv_win64.exe
xSAPFilePath=resources\\tools\\xSAP_win64.exe
\ No newline at end of file
plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/SSR_fi/.project 0 → 100644
+ 12
− 0
View file @ bb505aad
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
<name>SSR_fault</name>
<comment></comment>
<projects>
</projects>
<buildSpec>
</buildSpec>
<natures>
<nature>org.polarsys.chess.CHESSNature</nature>
</natures>
</projectDescription>
plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/SSR_fi/Documentation/MonitorPresence_MonitorPresenceIBD.svg 0 → 100644
+ 40
− 0
View file @ bb505aad
<?xml version="1.0" encoding="UTF-8"?><svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" stroke-dasharray="none" shape-rendering="auto" font-family="'Dialog'" width="520" text-rendering="auto" fill-opacity="1" contentScriptType="text/ecmascript" color-interpolation="auto" color-rendering="auto" preserveAspectRatio="xMidYMid meet" font-size="12" viewBox="0 0 520 270" fill="black" stroke="black" image-rendering="auto" stroke-miterlimit="10" zoomAndPan="magnify" version="1.0" stroke-linecap="square" stroke-linejoin="miter" contentStyleType="text/css" font-style="normal" height="270" stroke-width="1" stroke-dashoffset="0" font-weight="normal" stroke-opacity="1">
<!--Generated by the Batik Graphics2D SVG Generator-->
<defs id="genericDefs"/>
<g>
<defs id="defs1">
<linearGradient x1="10" x2="10" y1="10" gradientUnits="userSpaceOnUse" y2="260" xlink:type="simple" xlink:actuate="onLoad" id="linearGradient1" xlink:show="other" spreadMethod="pad">
<stop stop-opacity="1" stop-color="white" offset="0%"/>
<stop stop-opacity="1" stop-color="rgb(195,215,221)" offset="100%"/>
</linearGradient>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath1">
<path d="M10 10 L10 259 L509 259 L509 10 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath2">
<path d="M229 12 L292 12 L292 39 L229 39 L229 12 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath3">
<path d="M10 38 L511 38 L511 65 L10 65 L10 38 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath4">
<path d="M202 38 L338 38 L338 65 L202 65 L202 38 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath5">
<path d="M10 64 L511 64 L511 261 L10 261 L10 64 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath6">
<path d="M9 9 L511 9 L511 261 L9 261 L9 9 Z"/>
</clipPath>
</defs>
<g font-size="18" fill="url(#linearGradient1)" font-family="'Segoe UI'" stroke-linejoin="round" stroke="url(#linearGradient1)" stroke-width="0" stroke-miterlimit="0">
<rect x="10" y="10" clip-path="url(#clipPath1)" width="500" height="250" stroke="none"/>
<text x="230" y="33" clip-path="url(#clipPath2)" fill="black" stroke="none" xml:space="preserve">«Block»</text>
<image stroke="black" width="16" xlink:show="embed" xlink:type="simple" fill="black" clip-path="url(#clipPath3)" preserveAspectRatio="none" height="16" x="184" y="43" xlink:href="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAABAAAAAQCAYAAAAf8/9hAAABE0lEQVR42mNkgIKC&#13;&#10;BUf+P3jyCchiBOL/QMgIYTFCREDg/38GOFCU4WWYkGDDyAITuP/4E8OkNDsGYkHu&#13;&#10;rINgGm7Av7//GNjZmMHsEzceMVhoyDFYVK6EazjRHg4Xh2iAOIcJ2VQWZiawooKF&#13;&#10;x8FsELjQGwWXA4mD5GFyWAxgBCsCaQKxQcCgeBnDhHhLMB8kDjGcEbsBrECTQYpB&#13;&#10;mliRXADSBOLDDGNFcgE8DEBBzAo02ctEBWoYwgUwPkgzTP4fNAxYEPr/MTAzQTT5&#13;&#10;mqmC6btT41BCHiYOUY9mAAj4NWwCp4P/aCQMIFIIkM3IiGnA0govotNBTOd2zEAk&#13;&#10;B7BgM5VsA5aUew6gF1SUhEnyAkg9VQAAIP5fFwAMEf4AAAAASUVORK5CYII=" xlink:actuate="onLoad"/>
<text x="203" y="59" clip-path="url(#clipPath4)" fill="black" stroke="none" xml:space="preserve">MonitorPresence</text>
</g>
<g stroke-width="1.1" font-size="18" font-family="'Segoe UI'" stroke-linecap="butt">
<line clip-path="url(#clipPath5)" fill="none" x1="11" x2="511" y1="65" y2="65"/>
<rect x="10" y="10" clip-path="url(#clipPath6)" fill="none" width="499" rx="0" ry="0" height="249"/>
</g>
</g>
</svg>
plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/SSR_fi/Documentation/SpeedSensor_SpeedSensorIBD.svg 0 → 100644
+ 124
− 0
View file @ bb505aad
<?xml version="1.0" encoding="UTF-8"?><svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" stroke-dasharray="none" shape-rendering="auto" font-family="'Dialog'" width="870" text-rendering="auto" fill-opacity="1" contentScriptType="text/ecmascript" color-interpolation="auto" color-rendering="auto" preserveAspectRatio="xMidYMid meet" font-size="12" viewBox="0 0 870 270" fill="black" stroke="black" image-rendering="auto" stroke-miterlimit="10" zoomAndPan="magnify" version="1.0" stroke-linecap="square" stroke-linejoin="miter" contentStyleType="text/css" font-style="normal" height="270" stroke-width="1" stroke-dashoffset="0" font-weight="normal" stroke-opacity="1">
<!--Generated by the Batik Graphics2D SVG Generator-->
<defs id="genericDefs"/>
<g>
<defs id="defs1">
<linearGradient x1="20" x2="20" y1="10" gradientUnits="userSpaceOnUse" y2="260" xlink:type="simple" xlink:actuate="onLoad" id="linearGradient1" xlink:show="other" spreadMethod="pad">
<stop stop-opacity="1" stop-color="white" offset="0%"/>
<stop stop-opacity="1" stop-color="rgb(195,215,221)" offset="100%"/>
</linearGradient>
<linearGradient x1="10" x2="10" y1="80" gradientUnits="userSpaceOnUse" y2="100" xlink:type="simple" xlink:actuate="onLoad" id="linearGradient2" xlink:show="other" spreadMethod="pad">
<stop stop-opacity="1" stop-color="white" offset="0%"/>
<stop stop-opacity="1" stop-color="rgb(195,209,213)" offset="100%"/>
</linearGradient>
<linearGradient x1="510" x2="510" y1="98" gradientUnits="userSpaceOnUse" y2="118" xlink:type="simple" xlink:actuate="onLoad" id="linearGradient3" xlink:show="other" spreadMethod="pad">
<stop stop-opacity="1" stop-color="white" offset="0%"/>
<stop stop-opacity="1" stop-color="rgb(195,209,213)" offset="100%"/>
</linearGradient>
<linearGradient x1="510" x2="510" y1="187" gradientUnits="userSpaceOnUse" y2="207" xlink:type="simple" xlink:actuate="onLoad" id="linearGradient4" xlink:show="other" spreadMethod="pad">
<stop stop-opacity="1" stop-color="white" offset="0%"/>
<stop stop-opacity="1" stop-color="rgb(195,209,213)" offset="100%"/>
</linearGradient>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath1">
<path d="M20 10 L20 259 L519 259 L519 10 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath2">
<path d="M239 12 L302 12 L302 39 L239 39 L239 12 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath3">
<path d="M20 38 L521 38 L521 65 L20 65 L20 38 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath4">
<path d="M227 38 L334 38 L334 65 L227 65 L227 38 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath5">
<path d="M20 64 L521 64 L521 261 L20 261 L20 64 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath6">
<path d="M19 9 L521 9 L521 261 L19 261 L19 9 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath7">
<path d="M10 80 L10 99 L29 99 L29 80 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath8">
<path d="M10 80 L30 80 L30 100 L10 100 L10 80 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath9">
<path d="M9 79 L31 79 L31 101 L9 101 L9 79 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath10">
<path d="M39 79 L169 79 L169 106 L39 106 L39 79 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath11">
<path d="M58 79 L169 79 L169 106 L58 106 L58 79 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath12">
<path d="M39 59 L129 59 L129 86 L39 86 L39 59 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath13">
<path d="M510 98 L510 117 L529 117 L529 98 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath14">
<path d="M510 98 L530 98 L530 118 L510 118 L510 98 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath15">
<path d="M509 97 L531 97 L531 119 L509 119 L509 97 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath16">
<path d="M539 97 L744 97 L744 124 L539 124 L539 97 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath17">
<path d="M558 97 L744 97 L744 124 L558 124 L558 97 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath18">
<path d="M539 77 L629 77 L629 104 L539 104 L539 77 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath19">
<path d="M510 187 L510 206 L529 206 L529 187 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath20">
<path d="M510 187 L530 187 L530 207 L510 207 L510 187 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath21">
<path d="M509 186 L531 186 L531 208 L509 208 L509 186 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath22">
<path d="M539 186 L861 186 L861 213 L539 213 L539 186 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath23">
<path d="M558 186 L861 186 L861 213 L558 213 L558 186 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath24">
<path d="M539 166 L629 166 L629 193 L539 193 L539 166 Z"/>
</clipPath>
</defs>
<g font-size="18" fill="url(#linearGradient1)" font-family="'Segoe UI'" stroke-linejoin="round" stroke="url(#linearGradient1)" stroke-width="0" stroke-miterlimit="0">
<rect x="20" y="10" clip-path="url(#clipPath1)" width="500" height="250" stroke="none"/>
<text x="240" y="33" clip-path="url(#clipPath2)" fill="black" stroke="none" xml:space="preserve">«Block»</text>
<image stroke="black" width="16" xlink:show="embed" xlink:type="simple" fill="black" clip-path="url(#clipPath3)" preserveAspectRatio="none" height="16" x="209" y="43" xlink:href="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAABAAAAAQCAYAAAAf8/9hAAABE0lEQVR42mNkgIKC&#13;&#10;BUf+P3jyCchiBOL/QMgIYTFCREDg/38GOFCU4WWYkGDDyAITuP/4E8OkNDsGYkHu&#13;&#10;rINgGm7Av7//GNjZmMHsEzceMVhoyDFYVK6EazjRHg4Xh2iAOIcJ2VQWZiawooKF&#13;&#10;x8FsELjQGwWXA4mD5GFyWAxgBCsCaQKxQcCgeBnDhHhLMB8kDjGcEbsBrECTQYpB&#13;&#10;mliRXADSBOLDDGNFcgE8DEBBzAo02ctEBWoYwgUwPkgzTP4fNAxYEPr/MTAzQTT5&#13;&#10;mqmC6btT41BCHiYOUY9mAAj4NWwCp4P/aCQMIFIIkM3IiGnA0govotNBTOd2zEAk&#13;&#10;B7BgM5VsA5aUew6gF1SUhEnyAkg9VQAAIP5fFwAMEf4AAAAASUVORK5CYII=" xlink:actuate="onLoad"/>
<text x="228" y="59" clip-path="url(#clipPath4)" fill="black" stroke="none" xml:space="preserve">SpeedSensor</text>
</g>
<g stroke-width="1.1" font-size="18" font-family="'Segoe UI'" stroke-linecap="butt">
<line clip-path="url(#clipPath5)" fill="none" x1="21" x2="521" y1="65" y2="65"/>
<rect x="20" y="10" clip-path="url(#clipPath6)" fill="none" width="499" rx="0" ry="0" height="249"/>
<rect x="10" y="80" clip-path="url(#clipPath7)" fill="url(#linearGradient2)" width="20" height="20" stroke="none"/>
<image x="12" y="82" clip-path="url(#clipPath8)" width="16" xlink:href="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAABAAAAAQCAYAAAAf8/9hAAAAWUlEQVR42rWTSxIA&#13;&#10;MARDxf3vrN2YsUB9pvZ5ExEQEdoM03JKAAAyBqg4gjwBNyNkTkorZJByiBEEesYs&#13;&#10;qAy6PiM6RbIudSXeiEdFsuJWkTxxq0ieuB3il288meg1E7KJnvUAAAAASUVORK5C&#13;&#10;YII=" xlink:type="simple" xlink:actuate="onLoad" height="16" preserveAspectRatio="none" xlink:show="embed"/>
<rect x="10" y="80" clip-path="url(#clipPath9)" fill="none" width="19" rx="0" ry="0" height="19"/>
<image x="40" y="84" clip-path="url(#clipPath10)" width="16" xlink:href="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAABAAAAAQCAYAAAAf8/9hAAAAW0lEQVR42mNgGPKA&#13;&#10;EV3At2HLf0KaNjf4wPWxYFMwO98Zp+bUiXtR+EzEONMtvg+nHFEG7FpYhNMQFlJs&#13;&#10;BYnJG+kTZwDIVnTNIDGywwDdQJLDABdgISaqRgF+AACq4BszQ3y3cQAAAABJRU5E&#13;&#10;rkJggg==" xlink:type="simple" xlink:actuate="onLoad" height="16" preserveAspectRatio="none" xlink:show="embed"/>
<text xml:space="preserve" x="59" y="100" clip-path="url(#clipPath11)" stroke="none">in speed: Real</text>
<text xml:space="preserve" x="40" y="80" clip-path="url(#clipPath12)" stroke="none">«FlowPort»</text>
<rect x="510" y="98" clip-path="url(#clipPath13)" fill="url(#linearGradient3)" width="20" height="20" stroke="none"/>
<image x="512" y="100" clip-path="url(#clipPath14)" width="16" xlink:href="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAABAAAAAQCAYAAAAf8/9hAAAAWUlEQVR42rWTSxIA&#13;&#10;MARDxf3vrN2YsUB9pvZ5ExEQEdoM03JKAAAyBqg4gjwBNyNkTkorZJByiBEEesYs&#13;&#10;qAy6PiM6RbIudSXeiEdFsuJWkTxxq0ieuB3il288meg1E7KJnvUAAAAASUVORK5C&#13;&#10;YII=" xlink:type="simple" xlink:actuate="onLoad" height="16" preserveAspectRatio="none" xlink:show="embed"/>
<rect x="510" y="98" clip-path="url(#clipPath15)" fill="none" width="19" rx="0" ry="0" height="19"/>
<image x="540" y="102" clip-path="url(#clipPath16)" width="16" xlink:href="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAABAAAAAQCAYAAAAf8/9hAAAAW0lEQVR42mNgGPKA&#13;&#10;EV3At2HLf0KaNjf4wPWxYFMwO98Zp+bUiXtR+Ez4bHKL7yPoBSZ8mnctLCJoAAs+&#13;&#10;m9FdgM1ArAaAFBLrApxegBlCtgG4nEyUF9CjahTgBwD7PRrNf0tLJAAAAABJRU5E&#13;&#10;rkJggg==" xlink:type="simple" xlink:actuate="onLoad" height="16" preserveAspectRatio="none" xlink:show="embed"/>
<text xml:space="preserve" x="559" y="118" clip-path="url(#clipPath17)" stroke="none">out sensed_speed: Real</text>
<text xml:space="preserve" x="540" y="98" clip-path="url(#clipPath18)" stroke="none">«FlowPort»</text>
<rect x="510" y="187" clip-path="url(#clipPath19)" fill="url(#linearGradient4)" width="20" height="20" stroke="none"/>
<image x="512" y="189" clip-path="url(#clipPath20)" width="16" xlink:href="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAABAAAAAQCAYAAAAf8/9hAAAAWUlEQVR42rWTSxIA&#13;&#10;MARDxf3vrN2YsUB9pvZ5ExEQEdoM03JKAAAyBqg4gjwBNyNkTkorZJByiBEEesYs&#13;&#10;qAy6PiM6RbIudSXeiEdFsuJWkTxxq0ieuB3il288meg1E7KJnvUAAAAASUVORK5C&#13;&#10;YII=" xlink:type="simple" xlink:actuate="onLoad" height="16" preserveAspectRatio="none" xlink:show="embed"/>
<rect x="510" y="187" clip-path="url(#clipPath21)" fill="none" width="19" rx="0" ry="0" height="19"/>
<image x="540" y="191" clip-path="url(#clipPath22)" width="16" xlink:href="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAABAAAAAQCAYAAAAf8/9hAAAAW0lEQVR42mNgGPKA&#13;&#10;EV3At2HLf0KaNjf4wPWxYFMwO98Zp+bUiXtR+Ez4bHKL7yPoBSZ8mnctLCJoAAs+&#13;&#10;m9FdgM1ArAaAFBLrApxegBlCtgG4nEyUF9CjahTgBwD7PRrNf0tLJAAAAABJRU5E&#13;&#10;rkJggg==" xlink:type="simple" xlink:actuate="onLoad" height="16" preserveAspectRatio="none" xlink:show="embed"/>
<text xml:space="preserve" x="559" y="207" clip-path="url(#clipPath23)" stroke="none">out sensed_speed_is_present: Boolean</text>
<text xml:space="preserve" x="540" y="187" clip-path="url(#clipPath24)" stroke="none">«FlowPort»</text>
</g>
</g>
</svg>
plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/SSR_fi/Documentation/SpeedSensor_SpeedSensor_ErrorModel_Sm.svg 0 → 100644
+ 164
− 0
View file @ bb505aad
<?xml version="1.0" encoding="UTF-8"?><svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" stroke-dasharray="none" shape-rendering="auto" font-family="'Dialog'" width="1072" text-rendering="auto" fill-opacity="1" contentScriptType="text/ecmascript" color-interpolation="auto" color-rendering="auto" preserveAspectRatio="xMidYMid meet" font-size="12" viewBox="0 0 1072 571" fill="black" stroke="black" image-rendering="auto" stroke-miterlimit="10" zoomAndPan="magnify" version="1.0" stroke-linecap="square" stroke-linejoin="miter" contentStyleType="text/css" font-style="normal" height="571" stroke-width="1" stroke-dashoffset="0" font-weight="normal" stroke-opacity="1">
<!--Generated by the Batik Graphics2D SVG Generator-->
<defs id="genericDefs"/>
<g>
<g font-size="18" fill="url(#linearGradient1)" font-family="'Segoe UI'" stroke-linejoin="round" stroke="url(#linearGradient1)" stroke-width="0" stroke-miterlimit="0">
<rect x="53" y="53" clip-path="url(#clipPath1)" width="1009" height="508" stroke="none"/>
<text x="504" y="76" clip-path="url(#clipPath2)" fill="black" stroke="none" xml:space="preserve">«ErrorModel»</text>
<text x="488" y="102" clip-path="url(#clipPath3)" fill="black" stroke="none" xml:space="preserve">faultSpeedSensor</text>
<rect x="54" y="109" clip-path="url(#clipPath4)" fill="url(#linearGradient2)" width="1009" height="452" stroke="none"/>
<rect x="85" y="162" clip-path="url(#clipPath5)" fill="url(#linearGradient3)" width="20" opacity="0" height="20" stroke="none"/>
</g>
<svg xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:svg="http://www.w3.org/2000/svg" xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape" xmlns:cc="http://creativecommons.org/ns#" contentScriptType="text/ecmascript" zoomAndPan="magnify" contentStyleType="text/css" id="svg2" sodipodi:docname="round_full.svg" style="" version="1.1" width="20" preserveAspectRatio="xMidYMid meet" inkscape:version="0.48.5 r10040" height="20" class="" x="85" y="162">
<defs style="" id="defs4">
<linearGradient xlink:type="simple" style="" xlink:actuate="onLoad" id="linearGradient3789" xlink:show="other">
<stop id="stop3791" offset="0" style="stop-color:#000005;stop-opacity:1"/>
<stop id="stop3793" offset="1" style=" stop-color:black;stop-opacity:0"/>
</linearGradient>
<inkscape:perspective inkscape:persp3d-origin="42.5 : 13.333333 : 1" style="" id="perspective3063" inkscape:vp_z="85 : 20 : 1" inkscape:vp_y="0 : 1000 : 0" inkscape:vp_x="0 : 20 : 1" sodipodi:type="inkscape:persp3d"/>
<linearGradient xlink:type="simple" style="" xlink:actuate="onLoad" id="linearGradient3786" xlink:show="other">
<stop id="stop3788" offset="0" style=" stop-color:black;stop-opacity:0"/>
<stop id="stop3794" offset="1" style="stop-color:#919cd7;stop-opacity:1"/>
</linearGradient>
<linearGradient x1="53" x2="53" y1="53" gradientUnits="userSpaceOnUse" y2="561" xlink:type="simple" xlink:actuate="onLoad" id="linearGradient1" xlink:show="other" spreadMethod="pad">
<stop stop-opacity="1" stop-color="white" offset="0%"/>
<stop stop-opacity="1" stop-color="rgb(195,209,213)" offset="100%"/>
</linearGradient>
<linearGradient x1="54" x2="54" y1="109" gradientUnits="userSpaceOnUse" y2="561" xlink:type="simple" xlink:actuate="onLoad" id="linearGradient2" xlink:show="other" spreadMethod="pad">
<stop stop-opacity="1" stop-color="white" offset="0%"/>
<stop stop-opacity="1" stop-color="rgb(195,209,213)" offset="100%"/>
</linearGradient>
<linearGradient x1="85" x2="85" y1="162" gradientUnits="userSpaceOnUse" y2="182" xlink:type="simple" xlink:actuate="onLoad" id="linearGradient3" xlink:show="other" spreadMethod="pad">
<stop stop-opacity="1" stop-color="black" offset="0%"/>
<stop stop-opacity="1" stop-color="black" offset="100%"/>
</linearGradient>
<linearGradient x1="223" x2="223" y1="219" gradientUnits="userSpaceOnUse" y2="290" xlink:type="simple" xlink:actuate="onLoad" id="linearGradient4" xlink:show="other" spreadMethod="pad">
<stop stop-opacity="1" stop-color="white" offset="0%"/>
<stop stop-opacity="1" stop-color="rgb(195,209,213)" offset="100%"/>
</linearGradient>
<linearGradient x1="573" x2="573" y1="237" gradientUnits="userSpaceOnUse" y2="316" xlink:type="simple" xlink:actuate="onLoad" id="linearGradient5" xlink:show="other" spreadMethod="pad">
<stop stop-opacity="1" stop-color="white" offset="0%"/>
<stop stop-opacity="1" stop-color="rgb(195,209,213)" offset="100%"/>
</linearGradient>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath1">
<path d="M1050.9999 53 C1050.9999 53 1050.9999 53 1050.9999 53 L63 53 C57.4771 53 53 57.4772 53 63 L53 550 C53 555.5228 57.4771 559.9999 62.9999 559.9999 C62.9999 559.9999 63 559.9999 63 559.9999 L63 560 L1051 559.9999 C1056.5228 559.9999 1060.9999 555.5228 1060.9999 549.9999 L1061 550 L1060.9999 63 C1060.9999 63 1060.9999 63 1060.9999 63 C1060.9999 57.4771 1056.5228 53 1050.9999 53 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath2">
<path d="M503 55 L613 55 L613 82 L503 82 L503 55 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath3">
<path d="M487 81 L629 81 L629 108 L487 108 L487 81 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath4">
<path d="M53 108 L1063 108 L1063 562 L53 562 L53 108 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath5">
<path d="M85 162 L85 181 L104 181 L104 162 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath6">
<path d="M109 164 L168 164 L168 191 L109 191 L109 164 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath7">
<path d="M335 219 C335 219 335 219 335 219 L233 219 C227.4771 219 223 223.4772 223 229 L223 229 L223 279 C223 284.5228 227.4772 289 233 289 L335 289 C340.5228 289 345 284.5228 345 279 L345 279 L345 229 C345 223.4772 340.5228 219 335 219 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath8">
<path d="M252 221 L319 221 L319 248 L252 248 L252 221 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath9">
<path d="M222 218 L347 218 L347 291 L222 291 L222 218 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath10">
<path d="M728.9999 237 C728.9999 237 728.9999 237 728.9999 237 L582.9999 237 C577.4771 237 572.9999 241.4772 572.9999 247 L573 247 L573 305 C573 310.5228 577.4771 315 583 315 L729 315 C734.5228 315 738.9999 310.5228 738.9999 305 L739 305 L738.9999 247 C738.9999 247 738.9999 247 738.9999 247 C738.9999 241.4771 734.5228 237 728.9999 237 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath11">
<path d="M574 239 L741 239 L741 266 L574 266 L574 239 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath12">
<path d="M637 265 L678 265 L678 292 L637 292 L637 265 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath13">
<path d="M572 236 L741 236 L741 317 L572 317 L572 236 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath14">
<path d="M53 107 L1063 107 L1063 562 L53 562 L53 107 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath15">
<path d="M52 52 L1063 52 L1063 562 L52 562 L52 52 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath16">
<path d="M-1 -1 L1073 -1 L1073 572 L-1 572 L-1 -1 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath17">
<path d="M461 223 L512 223 L512 250 L461 250 L461 223 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath18">
<path d="M458 245 L465 245 L465 272 L458 272 L458 245 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath19">
<path d="M415 302 L532 302 L532 329 L415 329 L415 302 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath20">
<path d="M557 263 L575 263 L575 276 L557 276 L557 263 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath21">
<path d="M162 187 L258 187 L258 214 L162 214 L162 187 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath22">
<path d="M162 187 L169 187 L169 214 L162 214 L162 187 Z"/>
</clipPath>
<clipPath clipPathUnits="userSpaceOnUse" id="clipPath23">
<path d="M206 217 L225 217 L225 231 L206 231 L206 217 Z"/>
</clipPath>
</defs>
<sodipodi:namedview bordercolor="#666666" inkscape:window-height="1005" inkscape:zoom="5.6" id="base" inkscape:current-layer="layer1" style="" inkscape:window-y="-9" inkscape:cy="21.696429" inkscape:window-x="-9" inkscape:cx="-0.034771143" showgrid="false" inkscape:pageopacity="0.0" inkscape:document-units="px" units="px" inkscape:pageshadow="2" inkscape:window-width="1920" pagecolor="#ffffff" borderopacity="1.0" inkscape:window-maximized="1"/>
<metadata style="" id="metadata7">
<rdf:RDF style="">
<cc:Work rdf:about="" style="">
<dc:format style="">image/svg+xml</dc:format>
<dc:type style="" rdf:resource="http://purl.org/dc/dcmitype/StillImage"/>
<dc:title style=""/>
</cc:Work>
</rdf:RDF>
</metadata>
<g inkscape:groupmode="layer" id="layer1" style="" transform="translate(0,-1032.3617)" inkscape:label="Calque 1">
<path sodipodi:arg1="0.56068699" inkscape:flatsided="false" inkscape:randomized="0" sodipodi:type="star" d="M 17.5,14.821429 L 16.411844,16.226801 L 15.070423,17.392882 L 13.527285,18.274857 L 11.841734,18.838835 L 10.078543,19.063141 L 8.3054712,18.939156 L 6.5906569,18.471644 L 4.9999996,17.678572 L 3.5946269,16.590416 L 2.4285468,15.248994 L 1.5465709,13.705857 L 0.98259317,12.020305 L 0.75828691,10.257114 L 0.8822721,8.4840429 L 1.3497841,6.7692286 L 2.1428565,5.1785713 L 3.2310123,3.7731986 L 4.5724339,2.6071185 L 6.1155716,1.7251426 L 7.8011231,1.1611649 L 9.564314,0.93685861 L 11.337385,1.0608438 L 13.0522,1.5283558 L 14.642857,2.3214282 L 16.04823,3.409584 L 17.21431,4.7510056 L 18.096286,6.2941433 L 18.660263,7.9796948 L 18.88457,9.7428857 L 18.760584,11.515957 L 18.293073,13.230771 z" id="PapyrusPath" style="stroke-opacity:1; fill:black;fill-opacity:1;stroke:none" inkscape:rounded="0" transform="translate(0,1032.3617)" sodipodi:sides="16" sodipodi:r1="9.0667877" sodipodi:cx="9.8214283" sodipodi:cy="10" sodipodi:arg2="0.75703654" sodipodi:r2="9.0667877"/>
</g>
</svg>
<g stroke-miterlimit="0" stroke-width="0" font-size="18" font-family="'Segoe UI'" stroke-linejoin="round">
<text xml:space="preserve" x="110" y="185" clip-path="url(#clipPath6)" stroke="none"> Initial1</text>
<rect x="223" y="219" clip-path="url(#clipPath7)" fill="url(#linearGradient4)" width="123" height="71" stroke="none"/>
<text xml:space="preserve" x="253" y="242" clip-path="url(#clipPath8)" stroke="none">nominal</text>
</g>
<g stroke-width="1.1" font-size="18" font-family="'Segoe UI'" stroke-linecap="butt">
<rect x="223" y="219" clip-path="url(#clipPath9)" fill="none" width="122" rx="10" ry="10" height="70"/>
<rect x="573" y="237" clip-path="url(#clipPath10)" fill="url(#linearGradient5)" width="167" height="79" stroke="none"/>
<text xml:space="preserve" x="575" y="260" clip-path="url(#clipPath11)" stroke="none">«ErrorState, StuckAt»</text>
<text xml:space="preserve" x="638" y="286" clip-path="url(#clipPath12)" stroke="none">error</text>
<rect x="573" y="237" clip-path="url(#clipPath13)" fill="none" width="166" rx="10" ry="10" height="78"/>
<line clip-path="url(#clipPath14)" fill="none" x1="54" x2="1063" y1="108" y2="108"/>
<rect x="53" y="53" clip-path="url(#clipPath15)" fill="none" width="1008" rx="10" ry="10" height="507"/>
<line clip-path="url(#clipPath16)" fill="none" text-rendering="optimizeLegibility" x1="346" x2="573" y1="245" y2="271"/>
<text x="462" y="244" clip-path="url(#clipPath17)" text-rendering="optimizeLegibility" stroke="none" xml:space="preserve">failure</text>
<text x="459" y="266" clip-path="url(#clipPath18)" text-rendering="optimizeLegibility" stroke="none" xml:space="preserve"> </text>
<text x="416" y="323" clip-path="url(#clipPath19)" text-rendering="optimizeLegibility" stroke="none" xml:space="preserve">«InternalFault»</text>
<line clip-path="url(#clipPath20)" fill="none" text-rendering="optimizeLegibility" x1="558" x2="573" y1="274" y2="271"/>
<line clip-path="url(#clipPath20)" fill="none" text-rendering="optimizeLegibility" x1="573" x2="559" y1="271" y2="264"/>
<line clip-path="url(#clipPath16)" fill="none" text-rendering="optimizeLegibility" x1="103" x2="223" y1="170" y2="229"/>
<text x="163" y="208" clip-path="url(#clipPath21)" text-rendering="optimizeLegibility" stroke="none" xml:space="preserve">init_to_error</text>
<text x="163" y="208" clip-path="url(#clipPath22)" text-rendering="optimizeLegibility" stroke="none" xml:space="preserve"> </text>
<line clip-path="url(#clipPath23)" fill="none" text-rendering="optimizeLegibility" x1="207" x2="223" y1="227" y2="229"/>
<line clip-path="url(#clipPath23)" fill="none" text-rendering="optimizeLegibility" x1="223" x2="212" y1="229" y2="218"/>
<line clip-path="url(#clipPath16)" fill="none" text-rendering="optimizeLegibility" x1="103" x2="223" y1="170" y2="229"/>
<text x="163" y="208" clip-path="url(#clipPath21)" text-rendering="optimizeLegibility" stroke="none" xml:space="preserve">init_to_error</text>
<text x="163" y="208" clip-path="url(#clipPath22)" text-rendering="optimizeLegibility" stroke="none" xml:space="preserve"> </text>
<line clip-path="url(#clipPath23)" fill="none" text-rendering="optimizeLegibility" x1="207" x2="223" y1="227" y2="229"/>
<line clip-path="url(#clipPath23)" fill="none" text-rendering="optimizeLegibility" x1="223" x2="212" y1="229" y2="218"/>
<line clip-path="url(#clipPath16)" fill="none" text-rendering="optimizeLegibility" x1="346" x2="573" y1="245" y2="271"/>
<text x="462" y="244" clip-path="url(#clipPath17)" text-rendering="optimizeLegibility" stroke="none" xml:space="preserve">failure</text>
<text x="459" y="266" clip-path="url(#clipPath18)" text-rendering="optimizeLegibility" stroke="none" xml:space="preserve"> </text>
<text x="416" y="323" clip-path="url(#clipPath19)" text-rendering="optimizeLegibility" stroke="none" xml:space="preserve">«InternalFault»</text>
<line clip-path="url(#clipPath20)" fill="none" text-rendering="optimizeLegibility" x1="558" x2="573" y1="274" y2="271"/>
<line clip-path="url(#clipPath20)" fill="none" text-rendering="optimizeLegibility" x1="573" x2="559" y1="271" y2="264"/>
</g>
</g>
</svg>
plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/SSR_fi/MonolithicSmvFile/MonitorPresence.smv 0 → 100644
+ 23
− 0
View file @ bb505aad
MODULE main
VAR
State : { primary , t } ;
absence_alarm : boolean ;
input_is_present : boolean ;
enabled : boolean ;
FROZENVAR
InitTransition : { init_to_pr } ;
IVAR
Transition : { pr_to_pr } ;
INIT ( InitTransition = init_to_pr -> State = primary )
TRANS Transition = pr_to_pr -> ( ( TRUE ) & State = primary & next ( State ) = primary )
ASSIGN
init ( absence_alarm ) :=
case
InitTransition = init_to_pr : FALSE ;
esac ;
next ( absence_alarm ) :=
case
Transition = pr_to_pr & ( TRUE ) : ( !next(input_is_present) & next(enabled)) ;
TRUE : absence_alarm ;
esac ;
plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/SSR_fi/MonolithicSmvFile/Selector.smv 0 → 100644
+ 56
− 0
View file @ bb505aad
MODULE main
VAR
State : { input_1 , input_2 , t } ;
current_use : 1 .. 2 ;
output : real ;
output_is_present : boolean ;
input1 : real ;
input1_is_present : boolean ;
input2 : real ;
input2_is_present : boolean ;
switch_current_use : boolean ;
FROZENVAR
InitTransition : { init_to_in1 } ;
IVAR
Transition : { in1_to_in1 , in1_to_in2 , in2_to_in1 , in2_to_in2 } ;
INIT ( InitTransition = init_to_in1 -> State = input_1 )
TRANS Transition = in1_to_in1 -> ( ( ! switch_current_use ) & State = input_1 & next ( State ) = input_1 )
TRANS Transition = in1_to_in2 -> ( ( switch_current_use ) & State = input_1 & next ( State ) = input_2 )
TRANS Transition = in2_to_in1 -> ( ( switch_current_use ) & State = input_2 & next ( State ) = input_1 )
TRANS Transition = in2_to_in2 -> ( ( ! switch_current_use ) & State = input_2 & next ( State ) = input_2 )
ASSIGN
init ( current_use ) :=
case
InitTransition = init_to_in1 : 1 ;
esac ;
init ( output ) :=
case
InitTransition = init_to_in1 : 0 ;
esac ;
init ( output_is_present ) :=
case
InitTransition = init_to_in1 : TRUE ;
esac ;
next ( current_use ) :=
case
Transition = in1_to_in2 & ( switch_current_use ) : 2 ;
Transition = in2_to_in1 & ( switch_current_use ) : 1 ;
TRUE : current_use ;
esac ;
next ( output ) :=
case
Transition = in1_to_in1 & ( ! switch_current_use ) : input1 ;
Transition = in1_to_in2 & ( switch_current_use ) : input2 ;
Transition = in2_to_in1 & ( switch_current_use ) : input1 ;
Transition = in2_to_in2 & ( ! switch_current_use ) : input2 ;
TRUE : output ;
esac ;
next ( output_is_present ) :=
case
Transition = in1_to_in1 & ( ! switch_current_use ) : input1_is_present ;
Transition = in1_to_in2 & ( switch_current_use ) : input2_is_present ;
Transition = in2_to_in1 & ( switch_current_use ) : input1_is_present ;
Transition = in2_to_in2 & ( ! switch_current_use ) : input2_is_present ;
TRUE : output_is_present ;
esac ;
plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/SSR_fi/MonolithicSmvFile/SpeedSensor.smv 0 → 100644
+ 32
− 0
View file @ bb505aad
MODULE main
VAR
State : { primary , t } ;
sensed_speed : real ;
sensed_speed_is_present : boolean ;
speed : real ;
FROZENVAR
InitTransition : { init_to_primary } ;
IVAR
Transition : { pr_to_pr } ;
INIT ( InitTransition = init_to_primary -> State = primary )
TRANS Transition = pr_to_pr -> ( ( TRUE ) & State = primary & next ( State ) = primary )
ASSIGN
init ( sensed_speed ) :=
case
InitTransition = init_to_primary : 0 ;
esac ;
init ( sensed_speed_is_present ) :=
case
InitTransition = init_to_primary : TRUE ;
esac ;
next ( sensed_speed ) :=
case
Transition = pr_to_pr & ( TRUE ) : speed ;
TRUE : sensed_speed ;
esac ;
next ( sensed_speed_is_present ) :=
case
Transition = pr_to_pr & ( TRUE ) : TRUE ;
TRUE : sensed_speed_is_present ;
esac ;
plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/SSR_fi/MonolithicSmvFile/System.oss 0 → 100644
+ 80
− 0
View file @ bb505aad
@requires discrete-time
COMPONENT System system
INTERFACE
INPUT speed : real ;
OUTPUT sensed_speed : real ;
OUTPUT sensed_speed_is_present : boolean ;
CONTRACT Sense
assume : speed=0 & G ( ( next ( speed ) - speed ) <=1
and ( next ( speed ) - speed ) >=-1 ) ;
guarantee : /--we expect that:
- there is always a sensed speed
- the delta between the speed and the sensed speed is <= 2
--/
always ( ( sensed_speed - speed <= 2 ) and ( sensed_speed - speed >= - 2 ) and
sensed_speed_is_present ) ;
REFINEMENT
SUB sensor1 : SpeedSensor ;
SUB sensor2 : SpeedSensor ;
SUB selector : Selector ;
SUB monitor2 : MonitorPresence ;
SUB monitor1 : MonitorPresence ;
CONNECTION sensor2.speed := speed ;
CONNECTION sensor1.speed := speed ;
CONNECTION monitor2.input_is_present := sensor2.sensed_speed_is_present ;
CONNECTION monitor1.input_is_present := sensor1.sensed_speed_is_present ;
CONNECTION selector.input2 := sensor2.sensed_speed ;
CONNECTION selector.input1 := sensor1.sensed_speed ;
CONNECTION selector.input1_is_present := sensor1.sensed_speed_is_present ;
CONNECTION selector.input2_is_present := sensor2.sensed_speed_is_present ;
CONNECTION sensed_speed := selector.output ;
CONNECTION sensed_speed_is_present := selector.output_is_present ;
CONNECTION selector.switch_current_use := monitor1.absence_alarm or monitor2.absence_alarm ;
CONNECTION monitor1.enabled := ( selector.current_use=1 ) ;
CONNECTION monitor2.enabled := ( selector.current_use=2 ) ;
CONTRACT Sense REFINEDBY sensor1.Sense , sensor2.Sense , selector.Select , selector.Switch , monitor2.Monitor , monitor1.Monitor ;
COMPONENT SpeedSensor
INTERFACE
INPUT speed : real ;
OUTPUT sensed_speed : real ;
OUTPUT sensed_speed_is_present : boolean ;
CONTRACT Sense
assume : speed=0 & G ( ( next ( speed ) - speed ) <=1
and ( next ( speed ) - speed ) >=-1 ) ;
guarantee : /--we expect that:
- there is always a sensed speed
- the delta between the speed and the sensed speed is <= 1
--/
always ( ( sensed_speed - speed <= 1 ) and ( sensed_speed - speed >= - 1 ) and
sensed_speed_is_present ) ;
COMPONENT Selector
INTERFACE
INPUT input1 : real ;
INPUT input1_is_present : boolean ;
INPUT input2 : real ;
INPUT input2_is_present : boolean ;
INPUT switch_current_use : boolean ;
OUTPUT current_use : 1 .. 2 ;
OUTPUT output : real ;
OUTPUT output_is_present : boolean ;
CONTRACT Select
assume : true ;
guarantee : ( output=0 and output_is_present = TRUE ) and always ( ( next ( current_use=1 ) implies ( next ( output ) =input1 and next ( output_is_present ) =input1_is_present ) ) and ( next ( current_use=2 ) implies ( next ( output ) =input2 and next ( output_is_present ) =input2_is_present ) ) ) ;
CONTRACT Switch
assume : true ;
guarantee : /--we expect that :
- the switch of the sensor depends only on the input boolean port 'switch_current_use'
--/
always ( ( ( current_use=1 and switch_current_use ) implies next ( current_use ) =2 ) and ( ( current_use=2 and switch_current_use ) implies next ( current_use ) =1 ) and ( ( not switch_current_use ) implies not change ( current_use ) ) ) ;
COMPONENT MonitorPresence
INTERFACE
INPUT input_is_present : boolean ;
INPUT enabled : boolean ;
OUTPUT absence_alarm : boolean ;
CONTRACT Monitor
assume : input_is_present=TRUE ;
guarantee : /-- we expect that:
- an alarm is triggered whenever the monitor is enabled and the input is not present (is absent)
--/
always ( ( absence_alarm ) iff ( enabled and not ( input_is_present ) ) ) ;
\ No newline at end of file
plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/SSR_fi/MonolithicSmvFile/System_monolithic.smv 0 → 100644
+ 160
− 0
View file @ bb505aad
-- ===============================================================================
-- ===============================================================================
MODULE main
VAR
sensor1 : SpeedSensor;
sensor2 : SpeedSensor;
selector : Selector;
monitor2 : MonitorPresence;
monitor1 : MonitorPresence;
VAR
speed : real;
DEFINE
sensed_speed := selector.output;
sensed_speed_is_present := selector.output_is_present;
-- ===============================================================================
-- End of module
-- ===============================================================================
-- ===============================================================================
MODULE SpeedSensor
VAR
State : {primary, t};
sensed_speed : real;
sensed_speed_is_present : boolean;
speed : real;
IVAR
Transition : {pr_to_pr};
FROZENVAR
InitTransition : {init_to_primary};
ASSIGN
init(sensed_speed) := case
InitTransition = init_to_primary : 0;
esac;
init(sensed_speed_is_present) := case
InitTransition = init_to_primary : TRUE;
esac;
next(sensed_speed) := case
(Transition = pr_to_pr & TRUE) : speed;
TRUE : sensed_speed;
esac;
next(sensed_speed_is_present) := case
(Transition = pr_to_pr & TRUE) : TRUE;
TRUE : sensed_speed_is_present;
esac;
INIT (InitTransition = init_to_primary -> State = primary);
TRANS (Transition = pr_to_pr -> ((TRUE & State = primary) & next(State) = primary));
-- ===============================================================================
-- End of module
-- ===============================================================================
-- ===============================================================================
MODULE Selector
VAR
State : {input_1, input_2, t};
current_use : 1 .. 2;
output : real;
output_is_present : boolean;
input1 : real;
input1_is_present : boolean;
input2 : real;
input2_is_present : boolean;
switch_current_use : boolean;
IVAR
Transition : {in1_to_in1, in1_to_in2, in2_to_in1, in2_to_in2};
FROZENVAR
InitTransition : {init_to_in1};
ASSIGN
init(current_use) := case
InitTransition = init_to_in1 : 1;
esac;
init(output) := case
InitTransition = init_to_in1 : 0;
esac;
init(output_is_present) := case
InitTransition = init_to_in1 : TRUE;
esac;
next(current_use) := case
(Transition = in1_to_in2 & switch_current_use) : 2;
(Transition = in2_to_in1 & switch_current_use) : 1;
TRUE : current_use;
esac;
next(output) := case
(Transition = in1_to_in1 & !switch_current_use) : input1;
(Transition = in1_to_in2 & switch_current_use) : input2;
(Transition = in2_to_in1 & switch_current_use) : input1;
(Transition = in2_to_in2 & !switch_current_use) : input2;
TRUE : output;
esac;
next(output_is_present) := case
(Transition = in1_to_in1 & !switch_current_use) : input1_is_present;
(Transition = in1_to_in2 & switch_current_use) : input2_is_present;
(Transition = in2_to_in1 & switch_current_use) : input1_is_present;
(Transition = in2_to_in2 & !switch_current_use) : input2_is_present;
TRUE : output_is_present;
esac;
INIT (InitTransition = init_to_in1 -> State = input_1);
TRANS (Transition = in1_to_in1 -> ((!switch_current_use & State = input_1) & next(State) = input_1));
TRANS (Transition = in1_to_in2 -> ((switch_current_use & State = input_1) & next(State) = input_2));
TRANS (Transition = in2_to_in1 -> ((switch_current_use & State = input_2) & next(State) = input_1));
TRANS (Transition = in2_to_in2 -> ((!switch_current_use & State = input_2) & next(State) = input_2));
-- ===============================================================================
-- End of module
-- ===============================================================================
-- ===============================================================================
MODULE MonitorPresence
VAR
State : {primary, t};
absence_alarm : boolean;
input_is_present : boolean;
enabled : boolean;
IVAR
Transition : {pr_to_pr};
FROZENVAR
InitTransition : {init_to_pr};
ASSIGN
init(absence_alarm) := case
InitTransition = init_to_pr : FALSE;
esac;
next(absence_alarm) := case
(Transition = pr_to_pr & TRUE) : (!next(input_is_present) & next(enabled));
TRUE : absence_alarm;
esac;
INIT (InitTransition = init_to_pr -> State = primary);
TRANS (Transition = pr_to_pr -> ((TRUE & State = primary) & next(State) = primary));
-- ===============================================================================
-- End of module
-- ===============================================================================
plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/SSR_fi/MonolithicSmvFile/map.txt 0 → 100644
+ 3
− 0
View file @ bb505aad
MonitorPresence "C:\Users\Alberto\Google Drive\AMASS Project\ARTA_p1\eclipse\git_home\CHESS_FBK\plugins\contracts\org.polarsys.chess.contracts.verificationService.test.runtime\testOutput\MonitorPresence.smv"
Selector "C:\Users\Alberto\Google Drive\AMASS Project\ARTA_p1\eclipse\git_home\CHESS_FBK\plugins\contracts\org.polarsys.chess.contracts.verificationService.test.runtime\testOutput\Selector.smv"
SpeedSensor "C:\Users\Alberto\Google Drive\AMASS Project\ARTA_p1\eclipse\git_home\CHESS_FBK\plugins\contracts\org.polarsys.chess.contracts.verificationService.test.runtime\testOutput\SpeedSensor.smv"
plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/SSR_fi/NuSMV3-OCRA/Files/MonitorPresence.oss 0 → 100644
+ 8
− 0
View file @ bb505aad
@requires discrete-time
COMPONENT system
INTERFACE
INPUT input_is_present : boolean ;
INPUT enabled : boolean ;
OUTPUT absence_alarm : boolean ;
CONTRACT Monitor assume : true ; guarantee : always ( absence_alarm iff ( enabled and fall ( input_is_present ) ) ) ;
\ No newline at end of file
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment

Copyright © Eclipse Foundation, Inc. All Rights Reserved.     Privacy Policy | Terms of Use | Copyright Agent