CristalCaveGem » LustreC » Lustrec-Tests

add_subdirectory(safety)

cmake_minimum_required(VERSION 2.8.4)

include(FindUnixCommands)

set(GLOBAL_LUSTRE_FILES "")

LUSTREFILES(LFILES ${CMAKE_CURRENT_SOURCE_DIR} )

list(APPEND GLOBAL_LUSTRE_FILES ${LFILES})

FOREACH(lfile ${LFILES})

	get_filename_component(L ${lfile} NAME_WE)

	set(LUSTRE_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/${L}")

	file(COPY ${lfile}   DESTINATION  ${LUSTRE_OUTPUT_DIR})

	if(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}.lusi)

		file(COPY  ${L}.lusi DESTINATION  ${LUSTRE_OUTPUT_DIR})

	else()

		message("generate ${L}.lusi \n")

		Lustre_Compile(LUS_FILE ${lfile}

				NODE ""

				OPTS "-lusi")				

		set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})

		execute_process(RESULT_VARIABLE res 

					COMMAND ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}__${LUS_OPTS_CUT}} 

					WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})

		if(${res} STREQUAL "0")

			file(COPY  ${L}.lusi DESTINATION  ${LUSTRE_OUTPUT_DIR})

		else()

			message("${L}.lusi Error")

		endif()

	endif()

	if(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}_input_values)

		file(COPY  ${L}_input_values DESTINATION  ${LUSTRE_OUTPUT_DIR})

	elseif(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}.lusi)

		message("generate input_values \n")

		execute_process(RESULT_VARIABLE res 

					COMMAND ${JAVA_RUNTIME} -cp ${CMAKE_BINARY_DIR}/modules/ Generate_inputs_lusi top ${L}.lusi 1

					WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})

		if(${res} STREQUAL "0")

			file(COPY  ${L}_input_values DESTINATION  ${LUSTRE_OUTPUT_DIR})

		else()

			message("${L}_input_values Error")

		endif()

	endif()

	if(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}_output_values)

		file(COPY  ${L}_output_values DESTINATION  ${LUSTRE_OUTPUT_DIR})

	elseif(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}_input_values)

		message("generate output_values for reference \n")

		set(LUSTRE_NODE_OPT  "${L}")

		Lustre_Compile(LUS_FILE ${lfile}

						NODE ${LUSTRE_NODE_OPT} 

						OPTS ""

						DIR ${CMAKE_CURRENT_SOURCE_DIR})

		set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})

		execute_process(

					COMMAND ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}} 

					WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})			

		execute_process(

					COMMAND  make -f ${L}.makefile

					WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})	

		execute_process(RESULT_VARIABLE res 

					COMMAND ${BASH} -c "./${L}_${LUSTRE_NODE_OPT} < ${L}_input_values > ${L}_output_values"

					WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})	

		file(REMOVE ${L}_${LUSTRE_NODE_OPT} io_frontend.o ${L}.c ${L}.h ${L}.lusic ${L}.makefile ${L}.o ${L}_alloc.h ${L}_main.c ${L}_main.o )

		if(${res} STREQUAL "0")

			file(COPY  ${L}_output_values DESTINATION  ${LUSTRE_OUTPUT_DIR})

		else()

			message("${L} output_values Error")

		endif()

	endif()

ENDFOREACH()

FOREACH(lus_file ${GLOBAL_LUSTRE_FILES})

	get_filename_component(L ${lus_file} NAME_WE)

	set(LUSTRE_NODE_OPT  "${L}")

	#first combination :mpfr

	set(LUSTRE_OPTIONS_OPT "-mpfr" "100")

	set(EPSILON "0.0001")

	# First command generate C files from Lustre file

	Lustre_Compile(LUS_FILE ${lus_file}

					NODE ${LUSTRE_NODE_OPT}

					OPTS ${LUSTRE_OPTIONS_OPT}

					CALL_ID "2")

	set(LUS_OPTS_CUT_2 "${LUSTRE_OPTS_POSTFIX_${L}_2}")

	add_test(NAME safety_plane_archi_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}

			COMMAND  ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}} 

	)

	 #********************* make -f ${L}.makefile ***************************

	 add_test(NAME safety_plane_archi_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}

			COMMAND  make -f ${L}.makefile

			WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}}

	)

	SET_TESTS_PROPERTIES ( safety_plane_archi_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}

	 PROPERTIES DEPENDS safety_plane_archi_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}

				REQUIRED_FILES ${L}.makefile

				)

	 #************** execute C binary **********************************

	if (BASH)

		add_test(

			NAME safety_plane_archi_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2} 

			COMMAND ${BASH} -c "./${L}_${LUSTRE_NODE_OPT} < ../${L}_input_values > ${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}_outputs"

			WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}}

		)

		SET_TESTS_PROPERTIES ( safety_plane_archi_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}

			PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}

				DEPENDS safety_plane_archi_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2})

	else()

		message(FATAL_ERROR "Unknown shell command ${BASH} -c for ${CMAKE_HOST_SYSTEM_NAME}")

	endif()

	 #************** execute C binary **********************************

	 add_test(NAME safety_plane_archi_DIFF_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}

COMMAND ${JAVA_RUNTIME} -cp ${CMAKE_BINARY_DIR}/modules/ compare_lustrec_outputs ${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}_outputs ../${L}_output_values ${EPSILON}

	   WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}}

	)

	SET_TESTS_PROPERTIES ( safety_plane_archi_DIFF_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}

	 PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}_outputs

				DEPENDS safety_plane_archi_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2} )

ENDFOREACH()

add_custom_target(safety_plane_archi COMMAND ${CMAKE_CTEST_COMMAND} -R safety_plane_archi)

-- y is true if the property x is true at least n succesive times.

-- nb_times is a positive integer which increases by 1 each time x is true

-- and decreases by 1 each time x is false.

-- the idea was: x is the error output of a sensor and y has been true

-- if nb_times equals 0 again, perhaps the sensor is fine again

--@ requires n > 0;

--@ ensures (not x) => (not y);

--@ ensures nb_times >= 0;

--@ ensures not x => ((pre nb_times > nb_times) or (pre nb_times = 0));

--@ ensures x => (pre nb_times < nb_times);

--@ ensures y => nb_times >= n;

node check_validity (x: bool; n: int) returns (y: bool; nb_times: int);

var

compt: int;

let

  compt = (if x then 1 else 0) -> if x then pre compt + 1 else 0;

  y = (compt >= n);

  nb_times= (if x then 1 else 0) -> 

    if x then pre nb_times + 1 else 

      (if pre nb_times > 0 then pre nb_times - 1 else 0);

tel

-- at the beginning, y = x

-- once x is true, y is true until reset is true

-- if reset is true, y = x

--@ ensures reset => y=x;

--@ ensures x => y;

--@ ensures pre y and not reset => y;

node lock (x, reset: bool) returns (y: bool);

let

y = x -> if reset then x else x or pre y;

tel

-- combination of check_validity and lock

--@ requires n > 0;

--@ ensures x => y;

--@ ensures (pre y and not y) => (not x);

node check_validity_lock (x: bool; n: int) returns (y: bool);

var

  nb_times: int;

  er: bool;

let

	(er, nb_times) = check_validity(x, n);

	y = x or lock(er, (nb_times = 0));

tel

-- check if the input is not changing too fast

--@ requires delta > 0.;

--@ ensures abs_1(v - pre v) <= delta;

node check_speed (s, delta: real) returns (v: real);

let

	v = s -> if s - pre v > delta 

	      	 then 

		      pre v + delta

		 else 

		      if pre v - s > delta

		      then

			  pre v - delta 

		       else s;

tel

-- the classic absolute value function

--@ ensures y >= 0.0;

--@ ensures (x >= 0.0) => (x = y);

--@ ensures (x <= 0.0) => (x = -y);

node abs_1 (x: real) returns (y: real);

let

  y= if x>0.0 then x else -x;

tel

-- ensures that the ranged_val output is between min and max.

-- [min , max] is the legal interval where the value must be

-- [min - delta , max + delta] is the interval the input value is allowed to be

-- delta can match for instance with the uncertainty of measurement

-- satmax => value > max

-- satmin => value < min

-- "error" occurs if the input value is out of [min - delta, max + delta]

--@ requires delta > 0.0;

--@ requires min <= max;

--@ ensures min <= ranged_val and ranged_val <= max;

--@ ensures ((min <= value) and (value <= max)) => (ranged_val = value);

--@ ensures (value < min) => satmin;

--@ ensures (max < value) => satmax;

--@ ensures satmin => (value < min);

--@ ensures satmax => (max <= value);

--@ ensures value < min => ranged_val = min;

--@ ensures value > value => ranged_val = max;

--@ ensures error => satmin or satmax;

--@ ensures delta + max < value => error;

--@ ensures value < min - delta => error;

node ranged_value (value, min, max, delta: real) returns (ranged_val:real; satmin, satmax, error: bool);

let

  satmin = value < min;

  satmax = value > max;

  error = (value > max + delta) or (value < min - delta);

  ranged_val = if value > max then max else (if value < min then min else value);

tel

-- checks if the node "aberration" has valid outputs 

node obs_aberration(s1,s2,s3,delta: real; ab1,ab2,ab3: bool) 

returns (ok_ab1, ok_ab2, ok_ab3, ok_rev1, ok_rev2, ok_rev3: bool);

var

  diff12, diff13, diff23: real;

let

  diff12 = abs_1(s1 - s2);

  diff13 = abs_1(s1 - s3);

  diff23 = abs_1(s2 - s3);

  ok_ab1 = (ab1 => (diff12 > delta and diff13 > delta));

  ok_ab2 = (ab2 => (diff12 > delta and diff23 > delta));

  ok_ab3 = (ab3 => (diff13 > delta and diff23 > delta));

  ok_rev1 = ((diff12 > delta and diff13 > delta) => ab1 );

  ok_rev2 = ((diff12 > delta and diff23 > delta) => ab2);

  ok_rev3 = ((diff13 > delta and diff23 > delta) => ab3);

tel 

-- it checks to make sure that there is no aberrant input value

-- i.e. here, if there isn't a value which is too remote from the other two.

-- delta is a safe range

--@ requires delta > 0.0;

--@ ensures exists ok_ab1, ok_ab2, ok_ab3, ok_rev1, ok_rev2, ok_rev3: bool; (ok_ab1, ok_ab2, ok_ab3, ok_rev1, ok_rev2, ok_rev3) = (obs_aberration (s1,s2,s3,delta,ab1,ab2,ab3));

node aberration (s1,s2,s3, delta: real) returns (ab1, ab2, ab3: bool);

var

  diff12, diff13, diff23: real;

let

  diff12 = abs_1(s1 - s2);

  diff13 = abs_1(s1 - s3);

  diff23 = abs_1(s2 - s3);

  ab1 = (diff12 > delta) and (diff13 > delta);

  ab2 = (diff12 > delta) and (diff23 > delta);

  ab3 = (diff13 > delta) and (diff23 > delta);

tel

--@ ensures (nb_errors = 0) => not (e1 or e2 or e3);

--@ ensures not (e1 or e2 or e3) => (nb_errors = 0);

--@ ensures e1 or e2 or e3 => nb_errors >= 1;

--@ ensures e1 and e2 and e3 => (nb_errors = 3);

--@ ensures e1 and e2 and not e3 => (nb_errors = 2);

--@ ensures e1 and not e2 and e3 => (nb_errors = 2);

--@ ensures not e1 and e2 and e3 => (nb_errors = 2);

--@ ensures not e1 and not e2 and e3 => (nb_errors = 1);

--@ ensures not e1 and e2 and not e3 => (nb_errors = 1);

--@ ensures e1 and not e2 and not e3 => (nb_errors = 1);

--@ ensures nb_errors = 0 or nb_errors = 1 or nb_errors = 2 or nb_errors =3;

node nb_err_calc( e1, e2, e3: bool) returns (nb_errors: int);

let

  nb_errors = if e1 and e2 and e3 

          then 3

          else if (e1 and e2) or (e2 and e3) or (e1 and e3)

             then 2

             else if e1 or e2 or e3

                then 1

                else 0;

tel

--@ requires nb_err = 0 or nb_err = 1 or nb_err = 2 or nb_err = 3;

--@ requires nb_err = nb_err_calc(e1, e2, e3);

--@ ensures nb_err = 2 => (v = s1 or v = s2 or v = s3);

--@ ensures nb_err = 3 => (v = pre v);

--@ ensures (nb_err = 1 and e1) => v = (s2 + s3) / 2.0;

--@ ensures (nb_err = 1 and e2) => v = (s1 + s3) / 2.0;

--@ ensures (nb_err = 1 and e3) => v = (s1 + s2) / 2.0;

--@ ensures nb_err = 0 => v = (s1 + s2 + s3) / 3.0;

node calc_value (nb_err: int; e1, e2, e3: bool; s1, s2, s3: real) returns (v: real);

var

  previous_good_value, v1, v2, v3, di: real;

let

  previous_good_value = 0.0 -> pre v;

  di = if nb_err = 0

	then 3.0

	else 

	     if nb_err = 1

	     then 2.0

	     else 1.0;

  v1 = if e1 then 0.0 else s1;

  v2 = if e2 then 0.0 else s2;

  v3 = if e3 then 0.0 else s3;

  v = if nb_err = 3 

	then  previous_good_value

	else (v1 + v2 + v3) / di;

tel

--@ requires min <= max;

--@ ensures min <= v and v <= max;

--@ ensures s < min => v = min;

--@ ensures s > max => v = max;

--@ ensures (min <= s and s <= max) => v = s;

node range(s, min, max: real) returns (v: real);

let

	v = if s < min then min else if s > max then max else s;

tel

--@ requires min <= max;

--@ requires delta > 0.0;

--@ ensures min <= value and value <= max; 

--@ ensures 0 <= nb_errors and nb_errors <= 3;

--@ ensures nb_errors = 3 => value = pre value;

--@ ensures exists ok_stMin, ok_stMax, ok_revMin, ok_revMax: bool; (ok_stMin, ok_stMax, ok_revMin, ok_revMax) = obs_simple_voter(s1, s2, s3, min, max, delta, value, warning_stMax, warning_stMin);

node simple_voter (s1, s2, s3, min, max, delta: real) returns (value: real; warning_stMax, warning_stMin: bool; nb_errors:int);

var 

  sp_s1, sp_s2, sp_s3: real;

--  sp_er1, sp_er2, sp_er3: bool;

--  speed_error1, speed_error2, speed_error3: bool;

  r_s1, r_s2, r_s3: real;

  stmin1, stmin2, stmin3, stmax1, stmax2, stmax3: bool;

  errorRange1, errorRange2, errorRange3: bool; 

  error1, error2, error3: bool;

  ab1, ab2, ab3: bool;

  error_ab1, error_ab2, error_ab3: bool;

let

  sp_s1 = check_speed (s1, delta);

--  speed_error1 = check_validity_lock(sp_er1, 20);

  (r_s1, stmin1, stmax1, errorRange1) = ranged_value(sp_s1, min, max, delta);

  error1 = errorRange1 or check_validity_lock (errorRange1, 12);

  sp_s2 = check_speed (s2, delta);

--  speed_error2 = check_validity_lock(sp_er2, 20);

  (r_s2, stmin2, stmax2, errorRange2) = ranged_value(sp_s2, min, max, delta);

  error2 = errorRange2 or check_validity_lock (errorRange2, 14);

  sp_s3 = check_speed (s3, delta);

--  speed_error3 = check_validity_lock(sp_er3, 20);

  (r_s3, stmin3, stmax3, errorRange3) = ranged_value(sp_s3, min, max, delta);

  error3 = errorRange3 or check_validity_lock (errorRange3, 16);   

  warning_stMin = (stmin1 and stmin2) or (stmin1 and stmin3) or (stmin2 and stmin3);

  warning_stMax = (stmax1 and stmax2) or (stmax1 and stmax3) or (stmax2 and stmax3);

  (ab1, ab2, ab3) = if error1 or error2 or error3 

            then

              (error1, error2, error3)  

            else 

                aberration(r_s1, r_s2, r_s3, delta);

  error_ab1 = check_validity_lock (ab1, 16);  

  error_ab2 = check_validity_lock (ab2, 18);

  error_ab3 = check_validity_lock (ab3, 22);

  nb_errors = nb_err_calc(error_ab1, error_ab2, error_ab3);

  value = calc_value(nb_errors, error_ab1, error_ab2, error_ab3, r_s1, r_s2, r_s3);

tel

-- it checks if the warnings are valid

node obs_simple_voter(s1, s2, s3, min, max, delta, value: real; warning_stMax, warning_stMin: bool)

returns (ok_stMin, ok_stMax, ok_revMin, ok_revMax : bool);

var

  stmin1, stmin2, stmin3 : bool;

  stmax1, stmax2, stmax3 : bool;

let

  stmin1 = s1 < min - delta;

  stmin2 = s2 < min - delta;

  stmin3 = s3 < min - delta;

  stmax1 = s1 > max + delta;

  stmax2 = s2 > max + delta;

  stmax3 = s3 > max + delta;

  ok_stMin = (warning_stMin => ((stmin1 and stmin2) or (stmin2 and stmin3) or (stmin1 and stmin3)));  

  ok_stMax = (warning_stMax => ((stmax1 and stmax2) or (stmax2 and stmax3) or (stmax1 and stmax3)));

  ok_revMin = (((stmin1 and stmin2) or (stmin2 and stmin3) or (stmin1 and stmin3)) => warning_stMin); 

  ok_revMax = (((stmax1 and stmax2) or (stmax2 and stmax3) or (stmax1 and stmax3)) => warning_stMax);

tel

node voter_temp (s1, s2, s3: real) returns (value: real; warningMax, warningMin: bool; nb_err: int);

let

  (value, warningMin, warningMax, nb_err) = simple_voter (s1, s2, s3, 200.0, 2000.0, 80.0);

tel

node voter_alt (s1, s2, s3: real) returns (value: real; warningMax, warningMin: bool; nb_err: int);

let

  (value, warningMax, warningMin, nb_err) = simple_voter (s1, s2, s3, 0.0, 15000.0, 120.0);

tel

node safety_plane_archi(s1, s2, s3: real) returns (value: real; warningMax, warningMin: bool; nb_err: int);

let

  (value, warningMax, warningMin, nb_err) = simple_voter (s1, s2, s3, 0.0, 15000.0, 120.0);

tel

(* Generated Lustre Interface file from safety_plane_archi.lus *)

(* by Lustre-C compiler version 1.3-458, 2016/10/25, 14:3:40 *)

(* Feel free to mask some of the definitions by removing them from this file. *)

function abs_1 (x: real) returns (y: real);

node check_validity (x: bool; n: int) returns (y: bool; nb_times: int);

node lock (x: bool; reset: bool) returns (y: bool);

function aberration (s1: real; s2: real; s3: real; delta: real) returns (ab1: bool; ab2: bool; ab3: bool);

node calc_value (nb_err: int; e1: bool; e2: bool; e3: bool; s1: real; s2: real; s3: real) returns (v: real);

node check_speed (s: real; delta: real) returns (v: real);

node check_validity_lock (x: bool; n: int) returns (y: bool);

function nb_err_calc (e1: bool; e2: bool; e3: bool) returns (nb_errors: int);

function ranged_value (value: real; min: real; max: real; delta: real) returns (ranged_val: real; satmin: bool; satmax: bool; error: bool);

node simple_voter (s1: real; s2: real; s3: real; min: real; max: real; delta: real) returns (value: real; warning_stMax: bool; warning_stMin: bool; nb_errors: int);

function range (s: real; min: real; max: real) returns (v: real);

node voter_alt (s1: real; s2: real; s3: real) returns (value: real; warningMax: bool; warningMin: bool; nb_err: int);

node safety_plane_archi (s1: real; s2: real; s3: real) returns (value: real; warningMax: bool; warningMin: bool; nb_err: int);

function obs_simple_voter (s1: real; s2: real; s3: real; min: real; max: real; delta: real; value: real; warning_stMax: bool; warning_stMin: bool) returns (ok_stMin: bool; ok_stMax: bool; ok_revMin: bool; ok_revMax: bool);

function obs_aberration (s1: real; s2: real; s3: real; delta: real; ab1: bool; ab2: bool; ab3: bool) returns (ok_ab1: bool; ok_ab2: bool; ok_ab3: bool; ok_rev1: bool; ok_rev2: bool; ok_rev3: bool);

node voter_temp (s1: real; s2: real; s3: real) returns (value: real; warningMax: bool; warningMin: bool; nb_err: int);