plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/ParamArch/InstantiationResults/System1_instantiate.oss

@requires discrete-time

COMPONENT System1 system
INTERFACE
OUTPUT PORT output: integer;


CONTRACT Contract1Type
assume:
TRUE;
guarantee:
TRUE;

CONTRACT Contract2Type
assume:
TRUE;
guarantee:
TRUE;

CONTRACT Contract3Type
assume:
TRUE;
guarantee:
TRUE;

CONTRACT Contract4Type
assume:
TRUE;
guarantee:
 G output > 5;


REFINEMENT
SUB block_1[0]: Block;
SUB block_1[1]: Block;
SUB block_1[2]: Block;
SUB block_1[3]: Block;
CONNECTION block_1[0].inputPort := block_1[3].outputPort;
CONNECTION output := count(block_1[0].output, block_1[1].output, block_1[2].output, block_1[3].output);
CONNECTION block_1[1].inputPort := block_1[0].outputPort;
CONNECTION block_1[2].inputPort := block_1[1].outputPort;
CONNECTION block_1[3].inputPort := block_1[2].outputPort;

CONTRACT Contract2Type REFINEDBY block_1[0].Contract2Type, block_1[1].Contract2Type, block_1[2].Contract2Type, block_1[3].Contract2Type;
CONTRACT Contract3Type REFINEDBY block_1[0].Contract3Type, block_1[1].Contract3Type, block_1[2].Contract3Type, block_1[3].Contract3Type;
CONTRACT Contract4Type REFINEDBY block_1[0].Contract4Type, block_1[1].Contract4Type, block_1[2].Contract4Type, block_1[3].Contract4Type;
CONTRACT Contract1Type REFINEDBY block_1[0].Contract1Type, block_1[1].Contract1Type, block_1[2].Contract1Type, block_1[3].Contract1Type;


COMPONENT Block
INTERFACE
INPUT PORT inputPort: boolean;
OUTPUT PORT outputPort: boolean;
OUTPUT PORT 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:
 G output = TRUE;


REFINEMENT