CoCoSpec generation in stateless programs #1

-- This file has been generated by cocoSim


-- Properties nodes
node property_3_test_observer (In1_1_1 : real; In2_1_1 : real)
returns (Out1_1_1 : bool);
var
    LogicalOperator_1_1 : bool;
    LogicalOperator1_1_1 : bool;
    RelationalOperator_1_1 : bool;
    RelationalOperator1_1_1 : bool;
    RelationalOperator2_1_1 : bool;
    RelationalOperator3_1_1 : bool;
    Output2_1_1 : real;
    Output1_1_1 : real;
let
    LogicalOperator_1_1 = RelationalOperator_1_1 or RelationalOperator1_1_1;
    LogicalOperator1_1_1 = LogicalOperator_1_1 and RelationalOperator2_1_1 and RelationalOperator3_1_1;
    RelationalOperator_1_1 = Output1_1_1 >= In1_1_1;
    RelationalOperator1_1_1 = Output1_1_1 >= In2_1_1;
    RelationalOperator2_1_1 = Output2_1_1 >= In1_1_1;
    RelationalOperator3_1_1 = Output2_1_1 >= In2_1_1;
    Out1_1_1 = LogicalOperator1_1_1;

    (Output2_1_1, Output1_1_1) = property_3_test(In1_1_1, In2_1_1);
    --%PROPERTY Out1_1_1; 

tel


-- System nodes
node property_3_test (In1_1_1 : real; In2_1_1 : real)
returns (Out1_1_1 : real;
    Out2_2_1 : real); 
var
    Abs_1_1 : real;
    RelationalOperator_1_1 : bool;
    Switch_1_1 : real;
let 
    Abs_1_1 = if Switch_1_1 >= 0.0 then Switch_1_1 else -Switch_1_1;
    RelationalOperator_1_1 = In1_1_1 >= In2_1_1;
    Switch_1_1 = if RelationalOperator_1_1 then In1_1_1 else In2_1_1;
    Out1_1_1 = Switch_1_1;
    Out2_2_1 = Abs_1_1;
tel