CristalCaveGem » LustreC » Lustrec-Tests

-- This file has been generated by CoCoSim

-- Extern nodes

node ControlSys_SFunction (in1_1: int; in2_1: int)

returns (SFunction_1_1: int)

let

	--! c_code: mydouble;

SFunction_1_1 = 0;

tel

-- Properties nodes

node example1_SafetyProp (In1_1_1 : int; In2_1_1 : int)

returns (Out1_1_1 : bool);

var

	LogicalOperator_1_1 : bool;

	RelationalOperator_1_1 : bool;

	In5_1_1 : int;

	i_virtual_local : real;

let

	LogicalOperator_1_1 = RelationalOperator_1_1 and (In5_1_1 != 0);

	RelationalOperator_1_1 = In1_1_1 >= In2_1_1;

	Out1_1_1 = LogicalOperator_1_1;

	i_virtual_local= 0.0 -> 1.0;

	In5_1_1 = example1(In2_1_1, In1_1_1);

	--%PROPERTY Out1_1_1; 

tel

-- System nodes

node example1 (In1_1_1 : int; In2_1_1 : int)

returns (Out1_1_1 : int); 

var

	ControlSys_SFunction_1_1 : int;

	ControlSys_System_RelationalOperator_1_1 : bool;

	ControlSys_System_Switch_1_1 : int;

	i_virtual_local : real;

let 

	(ControlSys_SFunction_1_1) = ControlSys_SFunction(In1_1_1, In2_1_1);

	ControlSys_System_RelationalOperator_1_1 = In1_1_1 >= ControlSys_SFunction_1_1;

	ControlSys_System_Switch_1_1 = if ControlSys_System_RelationalOperator_1_1 then In1_1_1 else ControlSys_SFunction_1_1;

	Out1_1_1 = ControlSys_System_Switch_1_1;

	i_virtual_local= 0.0 -> 1.0;

tel

#include "mydouble.h"

int mydouble(int u, int w)

{

  return(u*w);

}

#ifndef _MYDOUBLE_H_

#define _MYDOUBLE_H_

int mydouble(int u, int w);

#endif

% Create the Legacy Code Tool data structure

def = legacy_code('initialize');

% Populate the data struture

def.SourceFiles = {'mydouble.c'};

def.HeaderFiles = {'mydouble.h'};

def.SFunctionName = 'legacy_mydouble';

def.OutputFcnSpec = 'int8 y1 = mydouble(int8 u1, int8 u2)';

def.SampleTime = [-1,0];

% Generate the S-function

legacy_code('sfcn_cmex_generate', def);

% Compile the MEX-file

legacy_code('compile', def);

% Generate a TLC-file

legacy_code('sfcn_tlc_generate', def);