diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/META-INF/MANIFEST.MF b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/META-INF/MANIFEST.MF index e69f135aae895473d6c620df6b7f3413e493191f..88262f68108e403a6372f939dd1c176f3d97e4be 100644 --- a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/META-INF/MANIFEST.MF +++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/META-INF/MANIFEST.MF @@ -34,7 +34,8 @@ Require-Bundle: eu.fbk.eclipse.standardtools.utils, eu.fbk.eclipse.standardtools.diagram.ui, eu.fbk.eclipse.standardtools.diagram, org.polarsys.chess.diagram.ui, - eu.fbk.tools.adapter.ui + eu.fbk.tools.adapter.ui, + org.polarsys.chess.OSSImporter Bundle-ActivationPolicy: lazy Import-Package: eu.fbk.eclipse.standardtools.logger, eu.fbk.tools.adapter.ui.preferences, diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/configTest.properties b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/configTest.properties index 38b8d29757161b533c4e2325ee12fabd0e453033..66bb512ab6af720519fe2df703da52075a0ae6c4 100644 --- a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/configTest.properties +++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/configTest.properties @@ -1,6 +1,6 @@ OCRAPath=C:\\Users\\Alberto\\Downloads\\20180124_OpenCertCHESSClient_Win_x64\\amass_P1\\FBK_Tools\\OCRA\\ocra_win64.exe testOutput=testOutput -testTempOutput=testTempOutput +testTempOutput=C:\\tmp\\adapter OCRAFilePath=resources\\tools\\ocra_win64.exe nuXmvFilePath=resources\\tools\\nuXmv_win64.exe xSAPFilePath=resources\\tools\\xSAP_win64.exe \ No newline at end of file diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/EmptyProject/.project b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/EmptyProject/.project new file mode 100644 index 0000000000000000000000000000000000000000..34eb0985d7cb41bbeef516f20e5c272837062552 --- /dev/null +++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/EmptyProject/.project @@ -0,0 +1,12 @@ +<?xml version="1.0" encoding="UTF-8"?> +<projectDescription> + <name>EmptyProject</name> + <comment></comment> + <projects> + </projects> + <buildSpec> + </buildSpec> + <natures> + <nature>org.polarsys.chess.CHESSNature</nature> + </natures> +</projectDescription> diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/EmptyProject/EmptyProject.di b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/EmptyProject/EmptyProject.di new file mode 100644 index 0000000000000000000000000000000000000000..8634d4c00e01da3a9ba292a8f51a6d39c79ee104 --- /dev/null +++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/EmptyProject/EmptyProject.di @@ -0,0 +1,2 @@ +<?xml version="1.0" encoding="UTF-8"?> +<xmi:XMI xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI"/> diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/EmptyProject/EmptyProject.notation b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/EmptyProject/EmptyProject.notation new file mode 100644 index 0000000000000000000000000000000000000000..8634d4c00e01da3a9ba292a8f51a6d39c79ee104 --- /dev/null +++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/EmptyProject/EmptyProject.notation @@ -0,0 +1,2 @@ +<?xml version="1.0" encoding="UTF-8"?> +<xmi:XMI xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI"/> diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/EmptyProject/EmptyProject.uml b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/EmptyProject/EmptyProject.uml new file mode 100644 index 0000000000000000000000000000000000000000..20ebfe46ba98f784f2c915ac476fe27a37239be8 --- /dev/null +++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/EmptyProject/EmptyProject.uml @@ -0,0 +1,364 @@ +<?xml version="1.0" encoding="UTF-8"?> +<xmi:XMI xmi:version="20131001" xmlns:xmi="http://www.omg.org/spec/XMI/20131001" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:CHESSViews="http://CHESS/Core/Views" xmlns:Core="http://CHESS/Core" xmlns:DependableComponent="http://CHESS/Dependability/DependableComponent" xmlns:ecore="http://www.eclipse.org/emf/2002/Ecore" xmlns:uml="http://www.eclipse.org/uml2/5.0.0/UML" xsi:schemaLocation="http://CHESS/Core/Views http://CHESS#//Core/CHESSViews http://CHESS/Core http://CHESS#//Core http://CHESS/Dependability/DependableComponent http://CHESS#//DependableComponent"> + <uml:Model xmi:id="_3PIH0MktEee0hNePRc2zdw" name="RootElement"> + <packagedElement xmi:type="uml:Package" xmi:id="_xRZHYMnYEeejHePP_Hzkeg" name="modelRequirementView"/> + <packagedElement xmi:type="uml:Package" xmi:id="_1irWYMnYEeejHePP_Hzkeg" name="modelSystemView"> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9i2i4MnhEeejHePP_Hzkeg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9i2i4cnhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#/"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_TZ_nULU5EduiKqCzJMWbGw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9i2i4snhEeejHePP_Hzkeg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9i2i48nhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//modelelements"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_Gx8MgLX7EduFmqQsrNB9lw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9i2i5MnhEeejHePP_Hzkeg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9i2i5cnhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//blocks"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_fSw28LX7EduFmqQsrNB9lw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9jTO0MnhEeejHePP_Hzkeg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9jTO0cnhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//portandflows"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_rpx28LX7EduFmqQsrNB9lw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9m4HQMnhEeejHePP_Hzkeg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9m4HQcnhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//constraints"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_5WYJ0LX7EduFmqQsrNB9lw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9m4HQsnhEeejHePP_Hzkeg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9m4HQ8nhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//activities"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_C2zXMLX8EduFmqQsrNB9lw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9m4HRMnhEeejHePP_Hzkeg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9m4HRcnhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//allocations"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_NxdG4LX8EduFmqQsrNB9lw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9oEaEMnhEeejHePP_Hzkeg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9oEaEcnhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//requirements"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_OOJC4LX8EduFmqQsrNB9lw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9pG74MnhEeejHePP_Hzkeg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9pG74cnhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//interactions"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_meOioLX8EduFmqQsrNB9lw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9pG74snhEeejHePP_Hzkeg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9pG748nhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//statemachines"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_nAF5kLX8EduFmqQsrNB9lw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_9pG75MnhEeejHePP_Hzkeg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_9pG75cnhEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//usecases"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_neZmMLX8EduFmqQsrNB9lw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_iBhF8M3gEeeAvtXJQCAINA"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_iBhF8c3gEeeAvtXJQCAINA" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://CHESS#//FailurePropagation"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_hdOrwLwzEd-CDNLmLgazUQ"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_iBqP4M3gEeeAvtXJQCAINA"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_iBqP4c3gEeeAvtXJQCAINA" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://CHESS#//ThreatsPropagation"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_5g4wEDQ3EeC0ueejuetpgA"/> + </profileApplication> + </packagedElement> + <packagedElement xmi:type="uml:Package" xmi:id="_otw4kMrMEee1tdS56VBt8w" name="modelComponentView"> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_OeWI4MrNEee1tdS56VBt8w"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_OeWI4crNEee1tdS56VBt8w" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/MARTE/1#//GRM"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://Papyrus_PROFILES/MARTE.profile.uml#_XVWGUAPMEdyuUt-4qHuVvQ"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_OeddoMrNEee1tdS56VBt8w"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_OeddocrNEee1tdS56VBt8w" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/MARTE/1#//Alloc"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://Papyrus_PROFILES/MARTE.profile.uml#_ar8OsAPMEdyuUt-4qHuVvQ"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_fxwU8MrOEee1tdS56VBt8w"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_fxwU8crOEee1tdS56VBt8w" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/MARTE/1#//VSL/DataTypes"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://Papyrus_PROFILES/MARTE.profile.uml#_9FdqwA-MEdyLh7muGbCqMw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_f3JC0MugEeemE4e81vDbeA"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_f3JC0cugEeemE4e81vDbeA" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://CHESS#//ComponentModel"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_MftccDQ2EeC0ueejuetpgA"/> + </profileApplication> + </packagedElement> + <packagedElement xmi:type="uml:Package" xmi:id="_JjGU4MrjEee1tdS56VBt8w" name="modeDeploymentView"/> + <packagedElement xmi:type="uml:Package" xmi:id="_CDbeUMrjEee1tdS56VBt8w" name="modelAnalysisView"> + <packagedElement xmi:type="uml:Package" xmi:id="_dNgC8MrjEee1tdS56VBt8w" name="modelDependabilityAnalysisView" URI=""> + <packagedElement xmi:type="uml:Package" xmi:id="_sDdU4E-yEemU0aMen8TVXg" name="modelSystemView_PhisicalArchitecture"> + <packagedElement xmi:type="uml:Component" xmi:id="_6WxCcE-yEemU0aMen8TVXg" name="FTA"/> + <packagedElement xmi:type="uml:Component" xmi:id="_e8vg0E-zEemU0aMen8TVXg" name="FTA"/> + <packagedElement xmi:type="uml:Component" xmi:id="_rDf3QE-zEemU0aMen8TVXg" name="CONTRACT_REF"/> + <packagedElement xmi:type="uml:Component" xmi:id="_8v_zsHe_EemmJfmKAb07HA" name="CONTRACT_COMPOSITE_IMPLEMENTATION_ANALYSIS_1"/> + <packagedElement xmi:type="uml:Component" xmi:id="_oEn0AHfDEemmJfmKAb07HA" name="FTA_ANALYSIS_1"/> + <packagedElement xmi:type="uml:Component" xmi:id="_dw9usHfKEemiWaxj_3Hy5w" name="FTA_ANALYSIS_2"/> + <packagedElement xmi:type="uml:Component" xmi:id="_8Khx4NnlEempZePwVoyTHA" name="CONTRACT_FTA"/> + <packagedElement xmi:type="uml:Component" xmi:id="_qnqwYNnrEempZePwVoyTHA" name="CONTRACT_IMPL"/> + <packagedElement xmi:type="uml:Component" xmi:id="_utBcMNnrEempZePwVoyTHA" name="PROP_VAL"/> + <packagedElement xmi:type="uml:Component" xmi:id="_yCJk8NnrEempZePwVoyTHA" name="CONT_PROP_VAL"/> + <packagedElement xmi:type="uml:Component" xmi:id="_0yqkwNnrEempZePwVoyTHA" name="MODEL_CHECK"/> + <packagedElement xmi:type="uml:Component" xmi:id="_4J37sNnsEempZePwVoyTHA" name="MODEL_CHECK"/> + </packagedElement> + <packagedElement xmi:type="uml:Class" xmi:id="_2Y9ZAMuXEee9L_NsVF0R0A" name="analisys_context"/> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_NZrioMuYEee9L_NsVF0R0A"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_NZ4-AMuYEee9L_NsVF0R0A" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/MARTE/1#//GQAM"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://Papyrus_PROFILES/MARTE.profile.uml#_4bV20APMEdyuUt-4qHuVvQ"/> + </profileApplication> + </packagedElement> + </packagedElement> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_3uHw8MktEee0hNePRc2zdw"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_3uSJAMktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#/"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_TZ_nULU5EduiKqCzJMWbGw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_4W8rgMktEee0hNePRc2zdw"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_4W8rgcktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//modelelements"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_Gx8MgLX7EduFmqQsrNB9lw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_4XGcgMktEee0hNePRc2zdw"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_4XGcgcktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//blocks"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_fSw28LX7EduFmqQsrNB9lw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_4XGcgsktEee0hNePRc2zdw"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_4XGcg8ktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//portandflows"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_rpx28LX7EduFmqQsrNB9lw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_4XGchMktEee0hNePRc2zdw"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_4XGchcktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//constraints"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_5WYJ0LX7EduFmqQsrNB9lw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_4XQNgMktEee0hNePRc2zdw"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_4XQNgcktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//activities"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_C2zXMLX8EduFmqQsrNB9lw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_4XQNgsktEee0hNePRc2zdw"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_4XQNg8ktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//allocations"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_NxdG4LX8EduFmqQsrNB9lw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_4XQNhMktEee0hNePRc2zdw"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_4XQNhcktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//requirements"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_OOJC4LX8EduFmqQsrNB9lw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_4XQNhsktEee0hNePRc2zdw"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_4XalkMktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//interactions"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_meOioLX8EduFmqQsrNB9lw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_4XalkcktEee0hNePRc2zdw"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_4XalksktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//statemachines"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_nAF5kLX8EduFmqQsrNB9lw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_4Xalk8ktEee0hNePRc2zdw"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_4XallMktEee0hNePRc2zdw" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/0.7.0/SysML#//usecases"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://SysML_PROFILES/SysML.profile.uml#_neZmMLX8EduFmqQsrNB9lw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_uI994MnYEeejHePP_Hzkeg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_uJHu4MnYEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://CHESS#//Core"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_ad4owDgVEd-68Z_bhNRGsA"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_uJRf4MnYEeejHePP_Hzkeg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_uJtkwMnYEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://CHESS#//Core/CHESSViews"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_FttqgMJDEd-0jpzjleFnug"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_bQEv0MnZEeejHePP_Hzkeg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_bQEv0cnZEeejHePP_Hzkeg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http:///CHESSContract.ecore#/"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSContract/CHESSContract.profile.uml#_Hmdm0NDVEeG5E52m3d5H1g"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_x0SGQMrOEee1tdS56VBt8w"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_x0bQMMrOEee1tdS56VBt8w" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/MARTE/1#//VSL/DataTypes"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://Papyrus_PROFILES/MARTE.profile.uml#_9FdqwA-MEdyLh7muGbCqMw"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_2nBfsMrSEee1tdS56VBt8w"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_2nLQsMrSEee1tdS56VBt8w" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://CHESS#//Safety"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_f-f6oMvrEeSajLw6mg2A8Q"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KFJm4E-zEemU0aMen8TVXg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KFLcEE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://CHESS#/"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_EA6IcDcwEd-mWLzcI61s7Q"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KGRBME-zEemU0aMen8TVXg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KGRoQE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://CHESS#//FailurePropagation"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_hdOrwLwzEd-CDNLmLgazUQ"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KGVSoE-zEemU0aMen8TVXg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KGYV8E-zEemU0aMen8TVXg" source="PapyrusVersion"> + <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_KGYV8U-zEemU0aMen8TVXg" key="Version" value="0.1.8"/> + <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_KGYV8k-zEemU0aMen8TVXg" key="Comment" value=""/> + <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_KGYV80-zEemU0aMen8TVXg" key="Copyright" value=""/> + <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_KGYV9E-zEemU0aMen8TVXg" key="Date" value="2010-09-24"/> + <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_KGYV9U-zEemU0aMen8TVXg" key="Author" value=""/> + </eAnnotations> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KGVSoU-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_QgRZcMe6Ed-7etIj5eTw0Q"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_cE_bwLwzEd-CDNLmLgazUQ"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KGZkEE-zEemU0aMen8TVXg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KGaLIE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://CHESS#//StateBasedComponents"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_d50lQL86Ed-TL8tpOyViyA"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KGfDoE-zEemU0aMen8TVXg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KGfDoU-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://CHESS#//FaultTolerance"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_mbqqgL86Ed-TL8tpOyViyA"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KGiG8E-zEemU0aMen8TVXg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KGiuAE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://CHESS#//MaintenanceMonitoring"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_oUVxcL88Ed-TL8tpOyViyA"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KGmYYE-zEemU0aMen8TVXg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KGm_cE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://CHESS#//StateBasedAnalysis"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_Wgxh0L8_Ed-TL8tpOyViyA"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KGpbsE-zEemU0aMen8TVXg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KGqCwE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://CHESS#//DependableComponent"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_uNKOgDQ2EeC0ueejuetpgA"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KGuUME-zEemU0aMen8TVXg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KGviUE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://CHESS#//ThreatsPropagation"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_5g4wEDQ3EeC0ueejuetpgA"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KG89sE-zEemU0aMen8TVXg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KG9kwE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://CHESS#//MitigationMeans"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_kJICMFiIEeGbwa2cK55fPQ"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KHABAE-zEemU0aMen8TVXg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KHEScE-zEemU0aMen8TVXg" source="PapyrusVersion"> + <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_KHEScU-zEemU0aMen8TVXg" key="Version" value="0.1.8"/> + <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_KHESck-zEemU0aMen8TVXg" key="Comment" value=""/> + <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_KHESc0-zEemU0aMen8TVXg" key="Copyright" value=""/> + <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_KHESdE-zEemU0aMen8TVXg" key="Date" value="2010-09-24"/> + <details xmi:type="ecore:EStringToStringMapEntry" xmi:id="_KHESdU-zEemU0aMen8TVXg" key="Author" value=""/> + </eAnnotations> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KHAoEE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_S2Uq0ce6Ed-7etIj5eTw0Q"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_nyQ7MLwzEd-CDNLmLgazUQ"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KHE5gE-zEemU0aMen8TVXg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KHFgkE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://CHESS#//HardwareBaseline"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_1TsX8MCpEd-RT45s8cwWMg"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KHH80E-zEemU0aMen8TVXg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KHH80U-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://CHESS#//RTComponentModel"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_WgatoDgVEd-68Z_bhNRGsA"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KHM1UE-zEemU0aMen8TVXg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KHNcYE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://CHESS#//ARINCComponentModel"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_GMlQEGwuEeWvYIaEJT1qow"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KHQfsE-zEemU0aMen8TVXg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KHRGwE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://CHESS#//ComponentModel"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_MftccDQ2EeC0ueejuetpgA"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_KHXNYE-zEemU0aMen8TVXg"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_KHX0cE-zEemU0aMen8TVXg" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://CHESS#//STS"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://CHESSML_PROFILE/CHESS.profile.uml#_-aQIUKbREeSHP5PnCeTneg"/> + </profileApplication> + <profileApplication xmi:type="uml:ProfileApplication" xmi:id="_ZLiWoILiEeqxuOOz6y6Ozw"> + <eAnnotations xmi:type="ecore:EAnnotation" xmi:id="_ZLjkwILiEeqxuOOz6y6Ozw" source="http://www.eclipse.org/uml2/2.0.0/UML"> + <references xmi:type="ecore:EPackage" href="http://www.eclipse.org/papyrus/MARTE/1#//GQAM"/> + </eAnnotations> + <appliedProfile xmi:type="uml:Profile" href="pathmap://Papyrus_PROFILES/MARTE.profile.uml#_4bV20APMEdyuUt-4qHuVvQ"/> + </profileApplication> + </uml:Model> + <Core:CHESS xmi:id="_vGqVMMnYEeejHePP_Hzkeg" base_Model="_3PIH0MktEee0hNePRc2zdw"/> + <CHESSViews:RequirementView xmi:id="_66csUMnYEeejHePP_Hzkeg" base_Package="_xRZHYMnYEeejHePP_Hzkeg"/> + <CHESSViews:SystemView xmi:id="_-r16UMnYEeejHePP_Hzkeg" base_Package="_1irWYMnYEeejHePP_Hzkeg"/> + <CHESSViews:ComponentView xmi:id="_vnH9EMrMEee1tdS56VBt8w" base_Package="_otw4kMrMEee1tdS56VBt8w"/> + <CHESSViews:DeploymentView xmi:id="_P-N-MMrjEee1tdS56VBt8w" base_Package="_JjGU4MrjEee1tdS56VBt8w"/> + <CHESSViews:AnalysisView xmi:id="_RhnDkMrjEee1tdS56VBt8w" base_Package="_CDbeUMrjEee1tdS56VBt8w"/> + <CHESSViews:DependabilityAnalysisView xmi:id="_oOsCwE-yEemU0aMen8TVXg" base_Package="_dNgC8MrjEee1tdS56VBt8w"/> + <DependableComponent:AnalysisContextElement xmi:id="_8wZcUHe_EemmJfmKAb07HA" type="CONTRACT_COMPOSITE_IMPLEMENTATION_ANALYSIS" date="Thu May 16 13:06:06 CEST 2019" valid="true" result="<?xml version="1.0" encoding="UTF-8"?>
<ns:OcraOutput xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="OcraOutput.xsd" xmlns:ns="https://es.fbk.eu/tools/ocra/xml/OcraOutput">
 <OcraResult checkType="ocra_check_refinement" timestamp="">
 <Component type="System">
 <Contract name="Sense">
 <CheckResult proofType="implementation" contractName="Sense">
 <Value value="OK"/>
 </CheckResult>
 <CheckResult proofType="environment" contractName="sensor1.Sense">
 <Value value="OK"/>
 </CheckResult>
 <CheckResult proofType="environment" contractName="sensor2.Sense">
 <Value value="OK"/>
 </CheckResult>
 <CheckResult proofType="environment" contractName="selector.Select">
 <Value value="OK"/>
 </CheckResult>
 <CheckResult proofType="environment" contractName="selector.Switch">
 <Value value="OK"/>
 </CheckResult>
 <CheckResult proofType="environment" contractName="monitor2.Monitor">
 <Value value="OK"/>
 </CheckResult>
 <CheckResult proofType="environment" contractName="monitor1.Monitor">
 <Value value="OK"/>
 </CheckResult>
 </Contract>
 </Component>
 </OcraResult>
 <OcraResult checkType="ocra_check_implementation" timestamp="">
 <Component type="Selector">
 <Contract name="Switch">
 <CheckResult> <Value value="OK"/>
 </CheckResult>
 </Contract>
 <Contract name="Select">
 <CheckResult> <Value value="OK"/>
 </CheckResult>
 </Contract>
 </Component>
 </OcraResult>
 <OcraResult checkType="ocra_check_implementation" timestamp="">
 <Component type="SpeedSensor">
 <Contract name="Sense">
 <CheckResult> <Value value="OK"/>
 </CheckResult>
 </Contract>
 </Component>
 </OcraResult>
 <OcraResult checkType="ocra_check_implementation" timestamp="">
 <Component type="MonitorPresence">
 <Contract name="Monitor">
 <CheckResult> <Value value="OK"/>
 </CheckResult>
 </Contract>
 </Component>
 </OcraResult>
</ns:OcraOutput>
" base_Component="_8v_zsHe_EemmJfmKAb07HA"/> + <DependableComponent:AnalysisContextElement xmi:id="_oEvIwHfDEemmJfmKAb07HA" type="FTA_ANALYSIS" date="Thu May 16 12:16:10 CEST 2019" valid="true" result="C:\Users\Alberto\git\CHESS_SystemArchitectureProjects_last\SSR_fi\VerificationResults\extended_RootElement_System_FTA_ANALYSIS_c1_2019-05-16-12-16-10.xml" base_Component="_oEn0AHfDEemmJfmKAb07HA"> + <conditions>property::sensor1.sensed_speed_is_present=TRUE</conditions> + </DependableComponent:AnalysisContextElement> + <DependableComponent:AnalysisContextElement xmi:id="_dxkLoHfKEemiWaxj_3Hy5w" type="FTA_ANALYSIS" date="Thu May 16 13:05:07 CEST 2019" valid="true" result="C:\Users\Alberto\git\CHESS_SystemArchitectureProjects_last\SSR_fi\VerificationResults\extended_RootElement_System_FTA_ANALYSIS_c1_2019-05-16-13-05-07.xml" base_Component="_dw9usHfKEemiWaxj_3Hy5w"> + <conditions>property::sensor1.sensed_speed_is_present=FALSE</conditions> + </DependableComponent:AnalysisContextElement> +</xmi:XMI> diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/EmptyProject/OssFile/System.oss b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/EmptyProject/OssFile/System.oss new file mode 100644 index 0000000000000000000000000000000000000000..cc5ad4b5d38ae7333ba4e21350890491e6141758 --- /dev/null +++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/EmptyProject/OssFile/System.oss @@ -0,0 +1,80 @@ + +@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 sensor2 : SpeedSensor ; +SUB monitor1 : MonitorPresence ; +SUB selector : Selector ; +SUB monitor2 : MonitorPresence ; +SUB sensor1 : SpeedSensor ; +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 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 ) ) ) ; +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 ) ) ) ; \ No newline at end of file diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestBasicOperations.java b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestBasicOperations.java index 0947bdd1b7f54311861a555838437794afc01568..fb6d5e77250cf5308e990ae72d42aa26867264da 100644 --- a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestBasicOperations.java +++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestBasicOperations.java @@ -13,6 +13,7 @@ import java.nio.file.attribute.BasicFileAttributes; import java.util.Collection; import java.util.HashMap; import java.util.HashSet; +import java.util.List; import java.util.Properties; import java.util.Set; import org.apache.commons.io.FileUtils; @@ -28,6 +29,8 @@ import org.eclipse.gmf.runtime.notation.Diagram; import org.eclipse.papyrus.junit.framework.classification.tests.AbstractPapyrusTest; import org.eclipse.papyrus.junit.utils.rules.PluginResource; import org.eclipse.papyrus.junit.utils.rules.ResourceSetFixture; +import org.eclipse.ui.IWorkbenchPage; +import org.eclipse.ui.PlatformUI; import org.eclipse.uml2.uml.Class; import org.eclipse.uml2.uml.Model; import org.eclipse.uml2.uml.Package; @@ -36,6 +39,7 @@ import org.junit.Before; import org.junit.Rule; import org.junit.Test; import org.junit.rules.ErrorCollector; +import org.polarsys.chess.OSSImporter.core.actions.ImportOSSFileAction; import org.polarsys.chess.contracts.profile.chesscontract.util.EntityUtil; import org.polarsys.chess.diagram.ui.services.CHESSDiagramsGeneratorService; import org.polarsys.chess.diagram.ui.services.ResultsGeneratorService; @@ -73,7 +77,6 @@ public class TestBasicOperations extends AbstractPapyrusTest { private final String projectFolderPath = "resources/SSR_fi/"; private final String projectPath = projectFolderPath + "SSR.di"; - @Rule public final ResourceSetFixture resourceSetFixture = new ResourceSetFixture(); @@ -137,17 +140,8 @@ public class TestBasicOperations extends AbstractPapyrusTest { ChessSystemModel chessSystemModel = ChessSystemModel.getInstance(); Model model = getModel(); - final org.eclipse.emf.ecore.resource.Resource resource = model.eResource(); - - URI resourceURI = resource.getURI(); - IWorkspace workspace = ResourcesPlugin.getWorkspace(); - IPath workspacePath = workspace.getRoot().getLocation(); - IPath finalPath = workspacePath.append(resourceURI.toPlatformString(false)); - final IFile[] files = ResourcesPlugin.getWorkspace().getRoot().findFilesForLocation(finalPath); - - // System.out.println("location: "+location); - IFile iFile = files[0]; - EntityUtil.getInstance().openCurrentModelIntoEditor(iFile); + + openEditor(model); OSSTranslatorServiceAPI ocraTranslatorService = OSSTranslatorServiceAPI.getInstance(chessSystemModel); @@ -208,6 +202,22 @@ public class TestBasicOperations extends AbstractPapyrusTest { } + + private void openEditor(final Model model) throws Exception { + final org.eclipse.emf.ecore.resource.Resource resource = model.eResource(); + + URI resourceURI = resource.getURI(); + IWorkspace workspace = ResourcesPlugin.getWorkspace(); + IPath workspacePath = workspace.getRoot().getLocation(); + IPath finalPath = workspacePath.append(resourceURI.toPlatformString(false)); + final IFile[] files = ResourcesPlugin.getWorkspace().getRoot().findFilesForLocation(finalPath); + + // System.out.println("location: "+location); + IFile iFile = files[0]; + EntityUtil.getInstance().openCurrentModelIntoEditor(iFile); + } + + @Before public void setTestParameters() throws Exception { testOutput = cleanDirectory("testOutput"); diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestBasicOperationsHeadless.java b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestBasicOperationsHeadless.java index 075617f71225203913d65c23b38c76d303542249..6fd20e6ec0c19af2426f27dd8656baa4ba02963f 100644 --- a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestBasicOperationsHeadless.java +++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestBasicOperationsHeadless.java @@ -14,9 +14,17 @@ import java.util.Properties; import java.util.Set; import org.apache.commons.io.FileUtils; import org.apache.log4j.Logger; +import org.eclipse.core.resources.IFile; +import org.eclipse.core.resources.IWorkspace; +import org.eclipse.core.resources.ResourcesPlugin; +import org.eclipse.core.runtime.IPath; import org.eclipse.core.runtime.NullProgressMonitor; +import org.eclipse.emf.common.util.URI; +import org.eclipse.emf.transaction.TransactionalEditingDomain; +import org.eclipse.emf.transaction.util.TransactionUtil; import org.eclipse.papyrus.junit.framework.classification.tests.AbstractPapyrusTest; import org.eclipse.papyrus.junit.framework.runner.Headless; +import org.eclipse.papyrus.junit.utils.rules.ModelSetFixture; import org.eclipse.papyrus.junit.utils.rules.PluginResource; import org.eclipse.papyrus.junit.utils.rules.ResourceSetFixture; import org.eclipse.uml2.uml.Class; @@ -27,6 +35,7 @@ import org.junit.Before; import org.junit.Rule; import org.junit.Test; import org.junit.rules.ErrorCollector; +import org.polarsys.chess.OSSImporter.core.actions.ImportOSSFileAction; import org.polarsys.chess.contracts.profile.chesscontract.util.EntityUtil; import org.polarsys.chess.service.core.model.ChessSystemModel; import org.polarsys.chess.service.core.model.UMLStateMachineModel; @@ -47,9 +56,15 @@ public class TestBasicOperationsHeadless extends AbstractPapyrusTest { private EntityUtil entityUtil = EntityUtil.getInstance(); private static final Logger logger = Logger.getLogger(TestBasicOperationsHeadless.class); + private final String emptyProjectFolderPath = "resources/EmptyProject/"; + private final String emptyProjectPath = "resources/EmptyProject/EmptyProject.di"; + private final String projectFolderPath = "resources/SSR_fi/"; private final String projectPath = projectFolderPath + "SSR.di"; + @Rule + public final ModelSetFixture modelSet = new ModelSetFixture(); + @Rule public final ResourceSetFixture resourceSetFixture = new ResourceSetFixture(); @@ -58,23 +73,83 @@ public class TestBasicOperationsHeadless extends AbstractPapyrusTest { public void testExportModelAsOss() throws Exception { Class umlSelectedComponent = getSystemComponent(); + File ossFile = exportModelAsOss(umlSelectedComponent, testOutput); + + String oracleFilePath = projectFolderPath + "NuSMV3-OCRA/Files/System.oss"; + compareTwoFilesIgnoreEOL(Paths.get(ossFile.getPath()), Paths.get(oracleFilePath)); + + } + + private void openEditor(final Model model) throws Exception { + final org.eclipse.emf.ecore.resource.Resource resource = model.eResource(); + + URI resourceURI = resource.getURI(); + IWorkspace workspace = ResourcesPlugin.getWorkspace(); + IPath workspacePath = workspace.getRoot().getLocation(); + IPath finalPath = workspacePath.append(resourceURI.toPlatformString(false)); + final IFile[] files = ResourcesPlugin.getWorkspace().getRoot().findFilesForLocation(finalPath); + + // System.out.println("location: "+location); + IFile iFile = files[0]; + EntityUtil.getInstance().openCurrentModelIntoEditor(iFile); + } + + @Test + @PluginResource(emptyProjectPath) + public void testImportModelFromOssFile() throws Exception{ + + Model model = getModel(); + + //openEditor(model); + + Package umlPackage = entityUtil.getSystemViewPackage(model); + //EntityUtil.getInstance().getCurrentSystemView(); + File ossInputFile = new File("resources//EmptyProject//OssFile//System.oss"); + + final ImportOSSFileAction action = ImportOSSFileAction.getInstance(); + + if (action != null) { + + // Hide the active page in order to avoid popups appearing + //final IWorkbenchPage activePage = PlatformUI.getWorkbench().getActiveWorkbenchWindow() + // .getActivePage(); + //activePage.setEditorAreaVisible(false); + //umlPackage = EntityUtil.getInstance().getCurrentSystemView(); + + TransactionalEditingDomain domain = modelSet.getEditingDomain(); + System.out.println("domain: "+domain); + // Parse the file and retrieve results + final StringBuffer importErrors = action.startParsing((Package) umlPackage, ossInputFile,domain); + + Class umlSelectedComponent = entityUtil.getSystemComponent(umlPackage); + //getSystemComponent(); + File ossFile = TestBasicOperationsHeadless.exportModelAsOss(umlSelectedComponent, testOutput); + + File outputFolder = new File(testOutput); + String selectedDirectory = outputFolder.getAbsolutePath(); + + String oracleFolder = emptyProjectFolderPath + "/OssFile"; + + verifyDirsAreEqual(Paths.get(oracleFolder), Paths.get(selectedDirectory)); + verifyDirsAreEqual(Paths.get(selectedDirectory), Paths.get(oracleFolder)); + + + } + } + + public static File exportModelAsOss(Class umlSelectedComponent,String testOutput) throws Exception { + OSSTranslatorServiceAPI ossTranslatorServiceAPI = OSSTranslatorServiceAPI .getInstance(ChessSystemModel.getInstance()); - System.out.println("umlSelectedComponent: " + umlSelectedComponent); - boolean temp_variable_is_discrete = true; - logger.debug("exportRootComponentAsOssModel"); Object ocraModel = ossTranslatorServiceAPI.exportRootComponentToOssModel(umlSelectedComponent, temp_variable_is_discrete, new NullProgressMonitor()); logger.debug("generateOssFileFromOssModel"); String fileName = ossTranslatorServiceAPI.getFileName(umlSelectedComponent); File ossFile = ossTranslatorServiceAPI.exportOSSModelToOSSFile(ocraModel, fileName, testOutput); - - String oracleFilePath = projectFolderPath + "NuSMV3-OCRA/Files/System.oss"; - compareTwoFilesIgnoreEOL(Paths.get(ossFile.getPath()), Paths.get(oracleFilePath)); - + return ossFile; } private Class getSystemComponent() throws Exception { diff --git a/plugins/org.polarsys.chess.OSSImporter/META-INF/MANIFEST.MF b/plugins/org.polarsys.chess.OSSImporter/META-INF/MANIFEST.MF index e1a270ce3209aa889ced294310a651497d265752..fb744d765c7493c37e1618102f3bcc04f87337f3 100644 --- a/plugins/org.polarsys.chess.OSSImporter/META-INF/MANIFEST.MF +++ b/plugins/org.polarsys.chess.OSSImporter/META-INF/MANIFEST.MF @@ -26,3 +26,4 @@ Import-Package: com.google.inject, org.apache.log4j;version="1.2.15", org.polarsys.chess.diagramsCreator.actions Bundle-Vendor: Fondazione Bruno Kessler +Export-Package: org.polarsys.chess.OSSImporter.core.actions diff --git a/plugins/org.polarsys.chess.OSSImporter/src/org/polarsys/chess/OSSImporter/commands/ImportOSSFileCommand.java b/plugins/org.polarsys.chess.OSSImporter/src/org/polarsys/chess/OSSImporter/commands/ImportOSSFileCommand.java index 4a9c9ca1636d88eec641e550cd1bf936d3247914..cc6f7f1be068939ebac15d4cec96c0274ef2a4b9 100644 --- a/plugins/org.polarsys.chess.OSSImporter/src/org/polarsys/chess/OSSImporter/commands/ImportOSSFileCommand.java +++ b/plugins/org.polarsys.chess.OSSImporter/src/org/polarsys/chess/OSSImporter/commands/ImportOSSFileCommand.java @@ -28,11 +28,14 @@ import org.eclipse.core.runtime.MultiStatus; import org.eclipse.core.runtime.Status; import org.eclipse.emf.ecore.EObject; import org.eclipse.emf.ecore.resource.Resource; +import org.eclipse.emf.transaction.TransactionalEditingDomain; +import org.eclipse.emf.transaction.util.TransactionUtil; import org.eclipse.gmf.runtime.diagram.ui.OffscreenEditPartFactory; import org.eclipse.gmf.runtime.diagram.ui.editparts.IGraphicalEditPart; import org.eclipse.gmf.runtime.notation.Diagram; import org.eclipse.jface.dialogs.ErrorDialog; import org.eclipse.jface.dialogs.MessageDialog; +import org.eclipse.papyrus.uml.tools.model.UmlModel; import org.eclipse.swt.SWT; import org.eclipse.swt.widgets.Display; import org.eclipse.swt.widgets.FileDialog; @@ -214,9 +217,13 @@ public class ImportOSSFileCommand extends AbstractJobCommand implements IHandler final IWorkbenchPage activePage = PlatformUI.getWorkbench().getActiveWorkbenchWindow() .getActivePage(); activePage.setEditorAreaVisible(false); - + //Resource resource = SelectionUtil.getInstance().getSelectedModelResource(); + + Package sysViewPkg = EntityUtil.getInstance().getCurrentSystemView(); + TransactionalEditingDomain domain = TransactionUtil.getEditingDomain(umlPackage); + // Parse the file and retrieve results - final StringBuffer importErrors = action.startParsing((Package) umlPackage, ossFile); + final StringBuffer importErrors = action.startParsing((Package) umlPackage, ossFile,domain); if (importErrors.length() != 0) { dialogUtil.showMessage_GenericMessage(DIALOG_TITLE, importErrors.toString()); } diff --git a/plugins/org.polarsys.chess.OSSImporter/src/org/polarsys/chess/OSSImporter/core/actions/ImportOSSFileAction.java b/plugins/org.polarsys.chess.OSSImporter/src/org/polarsys/chess/OSSImporter/core/actions/ImportOSSFileAction.java index 0e4842ac12c9862654b2cdc8f076597767f569e2..ecd15b7d17a402cd48d37ff8e5931a19da94ad3f 100644 --- a/plugins/org.polarsys.chess.OSSImporter/src/org/polarsys/chess/OSSImporter/core/actions/ImportOSSFileAction.java +++ b/plugins/org.polarsys.chess.OSSImporter/src/org/polarsys/chess/OSSImporter/core/actions/ImportOSSFileAction.java @@ -33,8 +33,6 @@ import org.polarsys.chess.contracts.profile.chesscontract.FormalProperty; import org.polarsys.chess.contracts.profile.chesscontract.util.ContractEntityUtil; import org.polarsys.chess.contracts.profile.chesscontract.util.EntityUtil; import org.polarsys.chess.service.core.model.ChessSystemModel; -import org.polarsys.chess.service.gui.utils.SelectionUtil; - import com.google.common.collect.Maps; import eu.fbk.eclipse.standardtools.ModelTranslatorToOcra.core.services.OSSModelFactory; @@ -82,10 +80,8 @@ import org.apache.log4j.Logger; import org.eclipse.emf.common.util.BasicEList; import org.eclipse.emf.common.util.EList; import org.eclipse.emf.ecore.EObject; -import org.eclipse.emf.ecore.resource.Resource; import org.eclipse.emf.transaction.RecordingCommand; import org.eclipse.emf.transaction.TransactionalEditingDomain; -import org.eclipse.emf.transaction.util.TransactionUtil; import org.eclipse.papyrus.sysml.portandflows.FlowDirection; /** @@ -1388,7 +1384,7 @@ public class ImportOSSFileAction { * @return * @throws Exception */ - public StringBuffer startParsing(Package pkg, File ossFile) throws Exception { + public StringBuffer startParsing(Package pkg, File ossFile, TransactionalEditingDomain domain) throws Exception { logger.debug("pkg: " + pkg); @@ -1447,12 +1443,13 @@ public class ImportOSSFileAction { // Clear the exception before starting the import importException = null; + // Start a transaction to modify the package content - Resource modelRes = SelectionUtil.getInstance().getSelectedModelResource(); - TransactionalEditingDomain domain = TransactionUtil.getEditingDomain(modelRes); - logger.debug("pkg.eResource(): " + pkg.eResource()); - logger.debug("pkg.eResource().getResourceSet(): " + pkg.eResource().getResourceSet()); - domain.getCommandStack().execute(new RecordingCommand(domain) { + //Resource modelRes = SelectionUtil.getInstance().getSelectedModelResource(); + //Package sysViewPkg = EntityUtil.getInstance().getCurrentSystemView(); + //TransactionalEditingDomain domain = TransactionUtil.getEditingDomain(pkg); + + domain.getCommandStack().execute(new RecordingCommand(domain) { @Override protected void doExecute() {