From 8d0d98205e5d52a1df458f6651839e15d670fdb4 Mon Sep 17 00:00:00 2001
From: Alberto Debiasi <adebiasi@fbk.eu>
Date: Wed, 29 Apr 2020 17:53:48 +0200
Subject: [PATCH] Add paramArch project .oss file.

Change-Id: I8e80e10ceef2b9ba1e4cda1da5afa02f56edc96f
---
 .../EmptyProject/ParamArch/System1.oss        | 41 +++++++++++++++++++
 1 file changed, 41 insertions(+)
 create mode 100644 plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/EmptyProject/ParamArch/System1.oss

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 000000000..b2b73cbcb
--- /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
-- 
GitLab