diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/EmptyProject/ParamArch/System1.oss b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/EmptyProject/ParamArch/System1.oss new file mode 100644 index 0000000000000000000000000000000000000000..b2b73cbcb36e10f8737be8163370757bae3bba28 --- /dev/null +++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/EmptyProject/ParamArch/System1.oss @@ -0,0 +1,41 @@ + +@requires discrete-time +COMPONENT System1 system +INTERFACE +OUTPUT output : integer ; +PARAMETER n_sub_comp : integer ; +CONTRACT Contract1Type +assume : TRUE ; +guarantee : TRUE ; +CONTRACT Contract2Type +assume : TRUE ; +guarantee : TRUE ; +CONTRACT Contract3Type +assume : TRUE ; +guarantee : TRUE ; +CONTRACT Contract4Type +assume : TRUE ; +guarantee : always ( output > 5 ) ; +REFINEMENT +SUB block_1 : array ( n_sub_comp ) of Block ; +CONNECTION block_1[i].inputPort := block_1[i - 1].outputPort for 1<=i<n_sub_comp ; +CONNECTION block_1[0].inputPort := block_1[n_sub_comp -1].outputPort ; +CONNECTION output := count ( for 0 <= i < n_sub_comp , block_1[i].output ) ; +CONTRACT Contract1Type REFINEDBY block_1[i].Contract1Type for 0 <= i <= ( n_sub_comp - 1 ) ; CONTRACT Contract2Type REFINEDBY block_1[i].Contract2Type for 0 <= i <= ( n_sub_comp - 1 ) ; CONTRACT Contract3Type REFINEDBY block_1[i].Contract3Type for 0 <= i <= ( n_sub_comp - 1 ) ; CONTRACT Contract4Type REFINEDBY block_1[i].Contract4Type for 0 <= i <= ( n_sub_comp - 1 ) ; +COMPONENT Block +INTERFACE +INPUT inputPort : boolean ; +OUTPUT outputPort : boolean ; +OUTPUT output : boolean ; +CONTRACT Contract1Type +assume : TRUE ; +guarantee : TRUE ; +CONTRACT Contract2Type +assume : TRUE ; +guarantee : TRUE ; +CONTRACT Contract3Type +assume : TRUE ; +guarantee : TRUE ; +CONTRACT Contract4Type +assume : TRUE ; +guarantee : always ( output = true ) ; \ No newline at end of file