diff --git a/compiler/global/global_printer.ml b/compiler/global/global_printer.ml index 89020f8..e3d1ee8 100644 --- a/compiler/global/global_printer.ml +++ b/compiler/global/global_printer.ml @@ -77,7 +77,7 @@ let rec print_static_exp_desc ff sed = match sed with | Sarray_power (se, n_list) -> fprintf ff "%a^%a" print_static_exp se (print_list print_static_exp """^""") n_list | Sarray se_list -> - fprintf ff "@[<2>%a@]" (print_list_r print_static_exp "["";""]") se_list + fprintf ff "@[<2>%a@]" (print_list_r print_static_exp "["",""]") se_list | Stuple se_list -> print_static_exp_tuple ff se_list | Srecord f_se_list -> print_record (print_couple print_qualname diff --git a/examples/MC_inlined/build b/examples/MC_inlined/build index 0683a08..695b556 100755 --- a/examples/MC_inlined/build +++ b/examples/MC_inlined/build @@ -1,6 +1,6 @@ #!/bin/bash HEPTC=../../heptc -HEPTC_OPTIONS="-flatten" +HEPTC_OPTIONS="" GCC=gcc GCC_OPTIONS="-g -O2 -std=c99 -I ../../../lib/c" @@ -9,7 +9,7 @@ VERBOSE=1 interfaces=(mctypes.epi) ext_libs=(mc_ext.epi mathext.epi) -sources=(mc.ept) +sources=() for f in ${interfaces[@]}; do if [ $VERBOSE ] ; then @@ -32,7 +32,7 @@ for f in ${sources[@]}; do $HEPTC $HEPTC_OPTIONS -target c $f done -#$HEPTC $HEPTC_OPTIONS -target c -s dv_fighterdebug mc.ept +$HEPTC $HEPTC_OPTIONS -target c -s dv_fighterdebug mcinlined.ept source_dirs=(mctypes_c mc_c) other_files=(main.c mathext.c mathext.h mc_ext.c mc_ext.h) diff --git a/examples/MC_inlined/mc.ept b/examples/MC_inlined/mc.ept index 2790e8c..93a0334 100644 --- a/examples/MC_inlined/mc.ept +++ b/examples/MC_inlined/mc.ept @@ -239,8 +239,8 @@ let if setnewtracknumber then currenttracknumber + 1 else currenttracknumber; previoustracknumber = fold <> missiontrackexist - (missiontrack^ksizemissiontracksarray, - previousmissiontracks, 0); + <(missiontrack)> + (previousmissiontracks, 0); newmissiontrack = setmissiontracknumber(missiontrack, if setnewtracknumber then newtracknumber @@ -449,8 +449,6 @@ let re_Output = not (re_Input -> pre re_Input) & re_Input; tel -const trackarrayinit : bool = false - (* safe state machine for the computing of radar or iff state state ident: state.0 *) node statecmd(onoffbuttonpressed : bool (*last = false*); @@ -858,8 +856,8 @@ node mc_tracks_prio(missiontracks : tmissiontracksarray) var prioritytracknumbers : tpriorityList; let missiontrackswithprio = - map<> prio_setpriorityinmissiontrackarray( - prioritytracknumbers^ksizemissiontracksarray, missiontracks); + map<> prio_setpriorityinmissiontrackarray + <(prioritytracknumbers)> (missiontracks); prioritytracknumbers = prio_selectprioritarymissiontracks(missiontracks, prio_selectprioritarymissiontracks(missiontracks, @@ -875,8 +873,8 @@ var l81 : int; let (withtracknumber, l81) = mapfold<> calculatemissiontracknumber - ((kinitmissiontrackarray -> pre withtracknumber)^ksizemissiontracksarray, - withouttracknb, 0 -> pre l81); + <(kinitmissiontrackarray -> pre withtracknumber)> + (withouttracknb, 0 -> pre l81); tel (* 1) merge tracks data received from both radar and iff sensors diff --git a/examples/MC_inlined/mcinlined.ept b/examples/MC_inlined/mcinlined.ept new file mode 100644 index 0000000..321b412 --- /dev/null +++ b/examples/MC_inlined/mcinlined.ept @@ -0,0 +1,1527 @@ +open Mctypes +open Mc_ext +open Mathext +node abs(a : float) returns (o : float) +let + o = if (<=.)(0.000000, a) then a else ~-.(a) +tel + +node sign(a : float) returns (o : float) +let + o = + if (>.)(a, 0.000000) + then 1.000000 + else if (=)(0.000000, a) then 0.000000 else ~-.(1.000000) +tel + +node myarctan(y : float; x : float) returns (atan : float) +var l6 : float; l4 : bool; l1 : float; +let + atan = + if l4 + then if (<.)(x, 0.000000) then (+.)(Mctypes.pi, l1) else l1 + else (Mctypes.pi /. 2.000000) *. sign(y); + l6 = if l4 then (/.)(y, x) else 0.000000 -> pre l6; + l4 = (>.)(abs(x), 0.100000); + l1 = Mathext.atanr(l6) +tel + +node missiontrackequalsprevious(previousone : Mctypes.tmissiontrack; + actualone : Mctypes.tmissiontrack) +returns (equal : bool) +let + equal = + (or) + ((&) + (not((=)(0, previousone.Mctypes.m_id)), + (=)(previousone.Mctypes.m_id, actualone.Mctypes.m_id)), + (&) + ((&) + ((<.) + (abs + ((-.) + (previousone.Mctypes.m_pos.Mctypes.x, + actualone.Mctypes.m_pos.Mctypes.x)) + , + 100.000000), + (<.) + (abs + ((-.) + (previousone.Mctypes.m_pos.Mctypes.y, + actualone.Mctypes.m_pos.Mctypes.y)) + , + 100.000000)) + , + not + ((&) + ((&) + ((&) + ((<.)(abs(previousone.Mctypes.m_pos.Mctypes.x), 0.100000), + (<.)(abs(previousone.Mctypes.m_pos.Mctypes.y), 0.100000)), + (<.)(abs(actualone.Mctypes.m_pos.Mctypes.x), 0.100000)), + (<.)(abs(actualone.Mctypes.m_pos.Mctypes.y), 0.100000))) + ) + ) + +tel + +node calctrackvisible1(position : Mctypes.tposition; speed : Mctypes.tspeed) +returns (trackvisible : bool) +let + trackvisible = + not + ((&) + ((&) + ((&) + ((<.)(abs(position.Mctypes.x), 0.001000), + (<.)(abs(position.Mctypes.y), 0.001000)), + (<.)(abs(speed.Mctypes.sx), 0.001000)), + (<.)(abs(speed.Mctypes.sy), 0.001000))) + +tel + +node missiontrackexist1(acc_tracknumber : int; + missiontrack : Mctypes.tmissiontrack; + previousmissiontrack : Mctypes.tmissiontrack) +returns (tracknumbertoset : int) +let + tracknumbertoset = + if (&) + (missiontrackequalsprevious(missiontrack, previousmissiontrack), + not((=)(0, previousmissiontrack.Mctypes.m_tracknumber))) + then previousmissiontrack.Mctypes.m_tracknumber + else acc_tracknumber +tel + +node missiontrackequalsprevious_orig(previousone : Mctypes.tmissiontrack; + actualone : Mctypes.tmissiontrack) +returns (equal : bool) +var l43 : bool; +let + l43 = not((=)(previousone.Mctypes.m_tracknumber, 0)); + equal = + (&) + (l43, + (or) + ((&) + ((&)(l43, not((=)(0, previousone.Mctypes.m_id))), + (=)(previousone.Mctypes.m_id, actualone.Mctypes.m_id)), + (&) + ((&) + ((<.) + (abs + ((-.) + (previousone.Mctypes.m_pos.Mctypes.x, + actualone.Mctypes.m_pos.Mctypes.x)) + , + 100.000000), + (<.) + (abs + ((-.) + (previousone.Mctypes.m_pos.Mctypes.y, + actualone.Mctypes.m_pos.Mctypes.y)) + , + 100.000000)) + , + not + ((&) + ((&) + ((&) + ((<.)(abs(previousone.Mctypes.m_pos.Mctypes.x), 0.100000), + (<.)(abs(previousone.Mctypes.m_pos.Mctypes.y), 0.100000)), + (<.)(abs(actualone.Mctypes.m_pos.Mctypes.x), 0.100000)), + (<.)(abs(actualone.Mctypes.m_pos.Mctypes.y), 0.100000))) + ) + ) + ) + +tel + +node util_radtodeg(input1 : float) returns (output1 : float) +let + output1 = (/.)(input1, (2.000000 *. Mctypes.pi)) *. 360.000000 +tel + +node util_degtorad(input1 : float) returns (output1 : float) +let + output1 = (/.)((2.000000 *. Mctypes.pi) *. input1, 360.000000) +tel + +node calctrackangle(speed : Mctypes.tspeed; + speedabs : Mctypes.tmetresseconde) +returns (trackangle : float) +var a : float; o : float; l51 : bool; l48 : float; l47 : float; +let + a = l47; + o = + if (>.)(a, 0.000000) + then 1.000000 + else if (=)(0.000000, a) then 0.000000 else ~-.(1.000000); + trackangle = + util_radtodeg(if l51 then 0.000000 else Mathext.acosr(l47) *. l48) *. + l48 *. + sign + (Mathext.asinr + ((/.)(speed.Mctypes.sy, if l51 then 1.000000 else speedabs))) + ; + l51 = (<.)(speedabs, 0.010000); + l48 = sign(l47); + l47 = (/.)(speed.Mctypes.sx, if l51 then 1.000000 else speedabs) +tel + +node calctrackvisible(position : Mctypes.tposition) +returns (trackvisible : bool) +let + trackvisible = + not + ((&) + ((<.)(abs(position.Mctypes.x), 0.001000), + (<.)(abs(position.Mctypes.y), 0.001000))) + +tel + +node missiontrackexist(missiontrack : Mctypes.tmissiontrack; + previousmissiontrack : Mctypes.tmissiontrack; + acc_tracknumber : int) +returns (tracknumbertoset : int) +var previousone : Mctypes.tmissiontrack; actualone : Mctypes.tmissiontrack; + equal : bool; +let + previousone = missiontrack; + actualone = previousmissiontrack; + equal = + (or) + ((&) + (not((=)(0, previousone.Mctypes.m_id)), + (=)(previousone.Mctypes.m_id, actualone.Mctypes.m_id)), + (&) + ((&) + ((<.) + (abs + ((-.) + (previousone.Mctypes.m_pos.Mctypes.x, + actualone.Mctypes.m_pos.Mctypes.x)) + , + 100.000000), + (<.) + (abs + ((-.) + (previousone.Mctypes.m_pos.Mctypes.y, + actualone.Mctypes.m_pos.Mctypes.y)) + , + 100.000000)) + , + not + ((&) + ((&) + ((&) + ((<.)(abs(previousone.Mctypes.m_pos.Mctypes.x), 0.100000), + (<.)(abs(previousone.Mctypes.m_pos.Mctypes.y), 0.100000)), + (<.)(abs(actualone.Mctypes.m_pos.Mctypes.x), 0.100000)), + (<.)(abs(actualone.Mctypes.m_pos.Mctypes.y), 0.100000))) + ) + ) + ; + tracknumbertoset = + if missiontrackequalsprevious(missiontrack, previousmissiontrack) + then previousmissiontrack.Mctypes.m_tracknumber + else acc_tracknumber +tel + +node calculatevrdivd(vr : float; d : float) returns (result : float) +var l13 : float; l11 : bool; +let + result = if l11 then l13 else 0.000000; + l13 = if l11 then (/.)(vr, d) else 0.000000 -> pre l13; + l11 = (>.)(d, 0.100000) +tel + +node trackalowerprioritythanb(a : Mctypes.tmissiontrack; + b : Mctypes.tmissiontrack) +returns (prioritary : bool) +let + prioritary = + (or) + ((or) + ((=)(a.Mctypes.m_targettype, Mctypes.Ttargettype_friend), + not(a.Mctypes.m_detectedbyradar)), + (&) + ((&) + (a.Mctypes.m_detectedbyradar, + (<.) + (calculatevrdivd(a.Mctypes.m_sr, a.Mctypes.m_d), + calculatevrdivd(b.Mctypes.m_sr, b.Mctypes.m_d))) + , + b.Mctypes.m_detectedbyradar)) + +tel + +node comparespeeds(speed1 : Mctypes.tspeed; speed2 : Mctypes.tspeed) +returns (equal : bool) +let + equal = + (&) + ((<.)(abs((-.)(speed1.Mctypes.sx, speed2.Mctypes.sx)), 1.000000), + (<.)(abs((-.)(speed1.Mctypes.sy, speed2.Mctypes.sy)), 1.000000)) +tel + +node calculateprioritizedtracknb(missiontrack : Mctypes.tmissiontrack) +returns (prioritizedtracknb : int) +let + prioritizedtracknb = + if (&) + (not + ((=)(missiontrack.Mctypes.m_targettype, Mctypes.Ttargettype_friend)), + not((=)(missiontrack.Mctypes.m_priority, 0))) + then missiontrack.Mctypes.m_tracknumber + else 0 +tel + +node sortreals(a : float; b : float) returns (newa : float; newb : float) +var l2 : bool; +let + l2 = (<.)(a, b); + newb = if l2 then a else b; + newa = if l2 then b else a +tel + +node comparepositions(pos1 : Mctypes.tposition; pos2 : Mctypes.tposition) +returns (equal : bool) +let + equal = + (&) + ((<.)(abs((-.)(pos1.Mctypes.x, pos2.Mctypes.x)), 0.100000), + (<.)(abs((-.)(pos1.Mctypes.y, pos2.Mctypes.y)), 0.100000)) +tel + +node comparetracks(pos1 : Mctypes.tposition; pos2 : Mctypes.tposition; + v1 : Mctypes.tspeed; v2 : Mctypes.tspeed) +returns (equal : bool) +let + equal = (&)(comparepositions(pos1, pos2), comparespeeds(v1, v2)) +tel + +node setmissiontracknumber(missiontrack : Mctypes.tmissiontrack; + number : int) +returns (newmissiontrack : Mctypes.tmissiontrack) +let + newmissiontrack = {missiontrack with .Mctypes.m_tracknumber = number} +tel + +node missiontrackisnull(missiontrack : Mctypes.tmissiontrack) +returns (isnull : bool) +var pos1 : Mctypes.tposition; pos2 : Mctypes.tposition; v1 : Mctypes.tspeed; + v2 : Mctypes.tspeed; equal : bool; +let + pos1 = missiontrack.Mctypes.m_pos; + pos2 = Mctypes.kInitPosition; + v1 = missiontrack.Mctypes.m_speed; + v2 = Mctypes.kInitSpeed; + equal = (&)(comparepositions(pos1, pos2), comparespeeds(v1, v2)); + isnull = + comparetracks + (missiontrack.Mctypes.m_pos, Mctypes.kInitPosition, + missiontrack.Mctypes.m_speed, Mctypes.kInitSpeed) +tel + +node calculatemissiontracknumber(previousmissiontracks : Mctypes.tmissiontracksarray; + missiontrack : Mctypes.tmissiontrack; + currenttracknumber : int) +returns (newmissiontrack : Mctypes.tmissiontrack; newtracknumber : int) +var missiontrack_2 : Mctypes.tmissiontrack; number : int; + newmissiontrack_2 : Mctypes.tmissiontrack; setnewtracknumber : bool; + previoustracknumber : int; +let + missiontrack_2 = missiontrack; + number = if setnewtracknumber then newtracknumber else previoustracknumber; + newmissiontrack_2 = {missiontrack_2 with .Mctypes.m_tracknumber = number}; + setnewtracknumber = + (&)((=)(previoustracknumber, 0), not(missiontrackisnull(missiontrack))); + newtracknumber = + if setnewtracknumber + then (+)(currenttracknumber, 1) + else currenttracknumber; + previoustracknumber = + fold<> missiontrackexist + <(missiontrack)>(previousmissiontracks, 0); + newmissiontrack = + setmissiontracknumber + (missiontrack, + if setnewtracknumber then newtracknumber else previoustracknumber) +tel + +node calculatetracktargettypefromid(id : int) +returns (targettype : Mctypes.ttargettype) +let + targettype = + if (=)(0, id) + then Mctypes.Ttargettype_unknown + else if (<=)(id, 500) + then Mctypes.Ttargettype_friend + else Mctypes.Ttargettype_foe + +tel + +node myderivative(inv : float; period : float) returns (o : float) +var l2 : float; +let + l2 = 0.000000 fby 0.000000 fby inv; + o = + if (or)((<.)(abs(l2), 0.100000), (<.)(abs(inv), 0.100000)) + then 0.000000 + else 0.000000 -> (/.)((-.)(inv, l2), 2.000000 *. period) +tel + +node calculatetrackspeedfrompos(position : Mctypes.tposition) +returns (speed : Mctypes.tspeed) +var inv_2 : float; period_2 : float; l2_2 : float; o_2 : float; inv : float; + period : float; l2 : float; o : float; +let + inv_2 = position.Mctypes.y; + period_2 = Mctypes.t; + l2_2 = 0.000000 fby 0.000000 fby inv_2; + o_2 = + if (or)((<.)(abs(l2_2), 0.100000), (<.)(abs(inv_2), 0.100000)) + then 0.000000 + else 0.000000 -> (/.)((-.)(inv_2, l2_2), 2.000000 *. period_2); + inv = position.Mctypes.x; + period = Mctypes.t; + l2 = 0.000000 fby 0.000000 fby inv; + o = + if (or)((<.)(abs(l2), 0.100000), (<.)(abs(inv), 0.100000)) + then 0.000000 + else 0.000000 -> (/.)((-.)(inv, l2), 2.000000 *. period); + speed = + { Mctypes.sx = + myderivative(position.Mctypes.x, Mctypes.t); + Mctypes.sy = + myderivative(position.Mctypes.y, Mctypes.t) } +tel + +node selectdetectedtrack(index : int; tracks : Mctypes.ttracksarray; + defaulttrack : Mctypes.ttrack) +returns (trackselected : Mctypes.ttrack) +let + trackselected = tracks.[index] default defaulttrack +tel + +node setmissiontrackpriority(missiontrack : Mctypes.tmissiontrack; + priority : int) +returns (newmissiontrack : Mctypes.tmissiontrack) +let + newmissiontrack = + {missiontrack with .Mctypes.m_priority = + if missiontrack.Mctypes.m_detectedbyradar then priority else 0} +tel + +node sortblockmissiontrack(a : Mctypes.tmissiontrack; + b : Mctypes.tmissiontrack) +returns (newa : Mctypes.tmissiontrack; newb : Mctypes.tmissiontrack) +var missiontrack : Mctypes.tmissiontrack; isnull : bool; l7 : bool; +let + missiontrack = a; + isnull = + comparetracks + (missiontrack.Mctypes.m_pos, Mctypes.kInitPosition, + missiontrack.Mctypes.m_speed, Mctypes.kInitSpeed); + l7 = missiontrackisnull(a); + newb = if l7 then a else b; + newa = if l7 then b else a +tel + +node sortblockpriorities(a : Mctypes.tmissiontrack; + b : Mctypes.tmissiontrack) +returns (newa : Mctypes.tmissiontrack; newb : Mctypes.tmissiontrack) +var a_2 : Mctypes.tmissiontrack; b_2 : Mctypes.tmissiontrack; + prioritary : bool; l25 : bool; +let + a_2 = a; + b_2 = b; + prioritary = + (or) + ((or) + ((=)(a_2.Mctypes.m_targettype, Mctypes.Ttargettype_friend), + not(a_2.Mctypes.m_detectedbyradar)), + (&) + ((&) + (a_2.Mctypes.m_detectedbyradar, + (<.) + (calculatevrdivd(a_2.Mctypes.m_sr, a_2.Mctypes.m_d), + calculatevrdivd(b_2.Mctypes.m_sr, b_2.Mctypes.m_d))) + , + b_2.Mctypes.m_detectedbyradar)) + ; + l25 = trackalowerprioritythanb(a, b); + newb = if l25 then a else b; + newa = if l25 then b else a +tel + +node position_equal(p1 : Mctypes.tposition; p2 : Mctypes.tposition) +returns (res : bool) +let + res = (&)((=)(p1.Mctypes.x, p2.Mctypes.x), (=)(p1.Mctypes.y, p2.Mctypes.y)) +tel + +node speed_equal(s1 : Mctypes.tspeed; s2 : Mctypes.tspeed) +returns (res : bool) +let + res = + (&)((=)(s1.Mctypes.sx, s2.Mctypes.sx), (=)(s1.Mctypes.sy, s2.Mctypes.sy)) +tel + +node convertifftracktomissiontrack(ifftrack : Mctypes.tifftrack) +returns (missiontrack : Mctypes.tmissiontrack) +var position_2 : Mctypes.tposition; trackvisible : bool; id : int; + targettype : Mctypes.ttargettype; position : Mctypes.tposition; + speed : Mctypes.tspeed; p1 : Mctypes.tposition; p2 : Mctypes.tposition; + res : bool; +let + position_2 = ifftrack.Mctypes.i_pos; + trackvisible = + not + ((&) + ((<.)(abs(position_2.Mctypes.x), 0.001000), + (<.)(abs(position_2.Mctypes.y), 0.001000))) + ; + id = ifftrack.Mctypes.i_id; + targettype = + if (=)(0, id) + then Mctypes.Ttargettype_unknown + else if (<=)(id, 500) + then Mctypes.Ttargettype_friend + else Mctypes.Ttargettype_foe + ; + position = ifftrack.Mctypes.i_pos; + speed = + { Mctypes.sx = + myderivative(position.Mctypes.x, Mctypes.t); + Mctypes.sy = + myderivative(position.Mctypes.y, Mctypes.t) }; + p1 = Mctypes.kInitPosition; + p2 = ifftrack.Mctypes.i_pos; + res = (&)((=)(p1.Mctypes.x, p2.Mctypes.x), (=)(p1.Mctypes.y, p2.Mctypes.y)); + missiontrack = + { Mctypes.m_pos = + ifftrack.Mctypes.i_pos; + Mctypes.m_speed = + if position_equal(Mctypes.kInitPosition, ifftrack.Mctypes.i_pos) + then Mctypes.kInitSpeed + else calculatetrackspeedfrompos(ifftrack.Mctypes.i_pos); + Mctypes.m_id = + ifftrack.Mctypes.i_id; + Mctypes.m_priority = + 0; + Mctypes.m_d = + 0.000000; + Mctypes.m_sabs = + 0.000000; + Mctypes.m_sr = + 0.000000; + Mctypes.m_detectedbyradar = + false; + Mctypes.m_detectedbyiff = + not + ((&) + (position_equal(ifftrack.Mctypes.i_pos, Mctypes.kInitPosition), + (=)(ifftrack.Mctypes.i_id, 0))) + ; + Mctypes.m_tracknumber = + 0; + Mctypes.m_targettype = + calculatetracktargettypefromid(ifftrack.Mctypes.i_id); + Mctypes.m_isvisible = + calctrackvisible(ifftrack.Mctypes.i_pos); + Mctypes.m_angle = + 0.000000 } +tel + +node convertrdrtracktomissiontrack(rdrtrack : Mctypes.trdrtrack) +returns (missiontrack : Mctypes.tmissiontrack) +var speed : Mctypes.tspeed; speedabs : Mctypes.tmetresseconde; l51 : bool; + l48 : float; l47 : float; trackangle : float; + position : Mctypes.tposition; trackvisible : bool; +let + speed = rdrtrack.Mctypes.r_s; + speedabs = rdrtrack.Mctypes.r_sabs; + trackangle = + util_radtodeg(if l51 then 0.000000 else Mathext.acosr(l47) *. l48) *. + l48 *. + sign + (Mathext.asinr + ((/.)(speed.Mctypes.sy, if l51 then 1.000000 else speedabs))) + ; + l51 = (<.)(speedabs, 0.010000); + l48 = sign(l47); + l47 = (/.)(speed.Mctypes.sx, if l51 then 1.000000 else speedabs); + position = rdrtrack.Mctypes.r_pos; + trackvisible = + not + ((&) + ((<.)(abs(position.Mctypes.x), 0.001000), + (<.)(abs(position.Mctypes.y), 0.001000))) + ; + missiontrack = + { Mctypes.m_pos = + rdrtrack.Mctypes.r_pos; + Mctypes.m_speed = + rdrtrack.Mctypes.r_s; + Mctypes.m_id = + 0; + Mctypes.m_priority = + 0; + Mctypes.m_d = + rdrtrack.Mctypes.r_d; + Mctypes.m_sabs = + rdrtrack.Mctypes.r_sabs; + Mctypes.m_sr = + rdrtrack.Mctypes.r_sr; + Mctypes.m_detectedbyradar = + not + ((&) + ((&) + ((&) + ((&) + (position_equal(rdrtrack.Mctypes.r_pos, Mctypes.kInitPosition), + speed_equal(rdrtrack.Mctypes.r_s, Mctypes.kInitSpeed)), + (=)(rdrtrack.Mctypes.r_d, 0.000000)), + (=)(rdrtrack.Mctypes.r_sabs, 0.000000)), + (=)(rdrtrack.Mctypes.r_sr, 0.000000))) + ; + Mctypes.m_detectedbyiff = + false; + Mctypes.m_tracknumber = + 0; + Mctypes.m_targettype = + Mctypes.Ttargettype_unknown; + Mctypes.m_isvisible = + calctrackvisible(rdrtrack.Mctypes.r_pos); + Mctypes.m_angle = + calctrackangle(rdrtrack.Mctypes.r_s, rdrtrack.Mctypes.r_sabs) } +tel + +node vectnorme(a : float; b : float) returns (c : float) +let + c = Mathext.sqrtr((+.)(a *. a, b *. b)) +tel + +node extracttrackposxy(track : Mctypes.ttrack) +returns (x : Mctypes.tmetres; y : Mctypes.tmetres) +let + y = track.Mctypes.t_pos.Mctypes.y; + x = track.Mctypes.t_pos.Mctypes.x +tel + +node elaboraterdrtrack(track : Mctypes.ttrack) +returns (rdrtrack : Mctypes.trdrtrack) +var position : Mctypes.tposition; speed : Mctypes.tspeed; a_2 : float; + b_2 : float; c_2 : float; a : float; b : float; c : float; + track_2 : Mctypes.ttrack; x_2 : Mctypes.tmetres; y_2 : Mctypes.tmetres; + d : float; v : float; vr : float; vx : float; vy : float; x : float; + y : float; l142 : Mctypes.tspeed; +let + position = { Mctypes.x = x; Mctypes.y = y }; + speed = + { Mctypes.sx = + myderivative(position.Mctypes.x, Mctypes.t); + Mctypes.sy = + myderivative(position.Mctypes.y, Mctypes.t) }; + a_2 = x; + b_2 = y; + c_2 = Mathext.sqrtr((+.)(a_2 *. a_2, b_2 *. b_2)); + a = vx; + b = vy; + c = Mathext.sqrtr((+.)(a *. a, b *. b)); + track_2 = track; + y_2 = track_2.Mctypes.t_pos.Mctypes.y; + x_2 = track_2.Mctypes.t_pos.Mctypes.x; + switch ((=)(d, 0.000000)) + | true + do + vr = 0.000000 + | false + var xnorm : float; ynorm : float; do + + ynorm = (/.)(y, d); + xnorm = (/.)(x, d); + vr = ~-.((+.)(vx *. xnorm, vy *. ynorm)) + end; + (x, y) = extracttrackposxy(track); + rdrtrack = + { Mctypes.r_pos = + { Mctypes.x = x; Mctypes.y = y }; + Mctypes.r_s = + { Mctypes.sx = vx; Mctypes.sy = vy }; + Mctypes.r_d = + d; + Mctypes.r_sabs = + v; + Mctypes.r_sr = + vr }; + v = vectnorme(vx, vy); + d = vectnorme(x, y); + vy = l142.Mctypes.sy; + vx = l142.Mctypes.sx; + l142 = calculatetrackspeedfrompos({ Mctypes.x = x; Mctypes.y = y }) +tel + +node risingEdge(re_Input : bool) returns (re_Output : bool) +let + re_Output = (&)(not(re_Input -> pre re_Input), re_Input) +tel + +node statecmd(onoffbuttonpressed : bool; currentstate : Mctypes.tsensorstate) +returns (onoffcmd : bool) +let + automaton + state Off + do + onoffcmd = false + unless + | (&)(onoffbuttonpressed, (=)(currentstate, Mctypes.TState_OFF)) then On + state On + do + onoffcmd = true + unless + | (&)(onoffbuttonpressed, (=)(currentstate, Mctypes.TState_ON)) then Off + end +tel + +node mc_rdrstatecmd(rdronoffbutton : bool; + currentrdrstate : Mctypes.tsensorstate) +returns (rdronoffcmd : bool) +var onoffbuttonpressed : bool; currentstate : Mctypes.tsensorstate; + onoffcmd : bool; +let + onoffbuttonpressed = risingEdge(rdronoffbutton); + currentstate = currentrdrstate; + automaton + state Off + do + onoffcmd = false + unless + | (&)(onoffbuttonpressed, (=)(currentstate, Mctypes.TState_OFF)) then On + state On + do + onoffcmd = true + unless + | (&)(onoffbuttonpressed, (=)(currentstate, Mctypes.TState_ON)) then Off + end; + rdronoffcmd = statecmd(risingEdge(rdronoffbutton), currentrdrstate) +tel + +node mc_iffstatecmd(iffonoffbutton : bool; + currentiffstate : Mctypes.tsensorstate) +returns (iffonoffcmd : bool) +var onoffbuttonpressed : bool; currentstate : Mctypes.tsensorstate; + onoffcmd : bool; +let + onoffbuttonpressed = risingEdge(iffonoffbutton); + currentstate = currentiffstate; + automaton + state Off + do + onoffcmd = false + unless + | (&)(onoffbuttonpressed, (=)(currentstate, Mctypes.TState_OFF)) then On + state On + do + onoffcmd = true + unless + | (&)(onoffbuttonpressed, (=)(currentstate, Mctypes.TState_ON)) then Off + end; + iffonoffcmd = statecmd(risingEdge(iffonoffbutton), currentiffstate) +tel + +node rdrmodecmd(currentstate : Mctypes.tsensorstate; + modebuttonpressed : bool; currentmode : Mctypes.trdrmode) +returns (modecmd : bool) +let + automaton + state Wide + do + modecmd = false + unless + | (&) + (modebuttonpressed, + (&) + ((=)(currentstate, Mctypes.TState_ON), + (=)(currentmode, Mctypes.TRdrMode_WIDE))) + then Narrow + state Narrow + do + modecmd = true + unless + | (&) + (modebuttonpressed, + (&) + ((=)(currentstate, Mctypes.TState_ON), + (=)(currentmode, Mctypes.TRdrMode_NARROW))) + then Wide + end +tel + +node mc_rdrmodecmd(currentrdrstate : Mctypes.tsensorstate; + rdrmodebutton : bool; currentrdrmode : Mctypes.trdrmode) +returns (rdrmodecmd : bool) +var currentstate : Mctypes.tsensorstate; modebuttonpressed : bool; + currentmode : Mctypes.trdrmode; modecmd : bool; +let + currentstate = currentrdrstate; + modebuttonpressed = risingEdge(rdrmodebutton); + currentmode = currentrdrmode; + automaton + state Wide + do + modecmd = false + unless + | (&) + (modebuttonpressed, + (&) + ((=)(currentstate, Mctypes.TState_ON), + (=)(currentmode, Mctypes.TRdrMode_WIDE))) + then Narrow + state Narrow + do + modecmd = true + unless + | (&) + (modebuttonpressed, + (&) + ((=)(currentstate, Mctypes.TState_ON), + (=)(currentmode, Mctypes.TRdrMode_NARROW))) + then Wide + end; + rdrmodecmd = + rdrmodecmd(currentrdrstate, risingEdge(rdrmodebutton), currentrdrmode) +tel + +node radar_mode(modecmd : bool) returns (mode : Mctypes.trdrmode) +let + mode = if modecmd then Mctypes.TRdrMode_NARROW else Mctypes.TRdrMode_WIDE +tel + +node radar_state(onoffcmd : bool; failure : bool) +returns (initializing : bool; st : Mctypes.tsensorstate) +var x : bool; +let + initializing = (&)((=)(st, Mctypes.TState_OFF), onoffcmd); + x = false fby false fby false fby false fby false fby onoffcmd; + st = + if failure + then Mctypes.TState_FAIL + else if if onoffcmd then x else false + then Mctypes.TState_ON + else Mctypes.TState_OFF + +tel + +node radar_tracks(st : Mctypes.tsensorstate; tracks : Mctypes.ttracksarray; + rdrdetectedtracks : Mctypes.tdetectedrdrtracksarray) +returns (rdrtracks : Mctypes.trdrtracksarray) +var l22 : Mctypes.ttrack^Mctypes.ksizerdrtracksarray; + l30 : Mctypes.trdrtrack^Mctypes.ksizerdrtracksarray; +let + rdrtracks = + if (=)(st, Mctypes.TState_ON) then l30 else Mctypes.kinitrdrtrackarray; + l30 = map<> elaboraterdrtrack<()>(l22); + l22 = + map<> selectdetectedtrack + <()>(rdrdetectedtracks, tracks^Mctypes.ksizerdrtracksarray, + Mctypes.kinittrack^Mctypes.ksizerdrtracksarray) +tel + +node radar(onoffcmd : bool; modecmd : bool; failure : bool; + rdrdetectedtracks : Mctypes.tdetectedrdrtracksarray; + tracks : Mctypes.ttracksarray) +returns (initializing : bool; st : Mctypes.tsensorstate; + mode : Mctypes.trdrmode; rdrtracks : Mctypes.trdrtracksarray) +var onoffcmd_2 : bool; failure_2 : bool; x : bool; initializing_2 : bool; + st_3 : Mctypes.tsensorstate; modecmd_2 : bool; mode_2 : Mctypes.trdrmode; + st_2 : Mctypes.tsensorstate; tracks_2 : Mctypes.ttracksarray; + rdrdetectedtracks_2 : Mctypes.tdetectedrdrtracksarray; + l22 : Mctypes.ttrack^Mctypes.ksizerdrtracksarray; + l30 : Mctypes.trdrtrack^Mctypes.ksizerdrtracksarray; + rdrtracks_2 : Mctypes.trdrtracksarray; +let + onoffcmd_2 = onoffcmd; + failure_2 = failure; + initializing_2 = (&)((=)(st_3, Mctypes.TState_OFF), onoffcmd_2); + x = false fby false fby false fby false fby false fby onoffcmd_2; + st_3 = + if failure_2 + then Mctypes.TState_FAIL + else if if onoffcmd_2 then x else false + then Mctypes.TState_ON + else Mctypes.TState_OFF + ; + modecmd_2 = modecmd; + mode_2 = + if modecmd_2 then Mctypes.TRdrMode_NARROW else Mctypes.TRdrMode_WIDE; + st_2 = st; + tracks_2 = tracks; + rdrdetectedtracks_2 = rdrdetectedtracks; + rdrtracks_2 = + if (=)(st_2, Mctypes.TState_ON) then l30 else Mctypes.kinitrdrtrackarray; + l30 = map<> elaboraterdrtrack<()>(l22); + l22 = + map<> selectdetectedtrack + <()>(rdrdetectedtracks_2, tracks_2^Mctypes.ksizerdrtracksarray, + Mctypes.kinittrack^Mctypes.ksizerdrtracksarray); + rdrtracks = radar_tracks(st, tracks, rdrdetectedtracks); + mode = radar_mode(modecmd); + (initializing, st) = radar_state(onoffcmd, failure) +tel + +node iff_state(onoffcmd : bool; failure : bool) +returns (initializing : bool; st : Mctypes.tsensorstate) +var x : bool; +let + initializing = (&)((=)(st, Mctypes.TState_OFF), onoffcmd); + x = false fby false fby false fby false fby false fby onoffcmd; + st = + if failure + then Mctypes.TState_FAIL + else if if onoffcmd then x else false + then Mctypes.TState_ON + else Mctypes.TState_OFF + +tel + +node ifftrack_of_track(track : Mctypes.ttrack) +returns (ifftrack : Mctypes.tifftrack) +let + ifftrack = + { Mctypes.i_pos = + track.Mctypes.t_pos; + Mctypes.i_id = + track.Mctypes.t_id } +tel + +node iff_tracks(st : Mctypes.tsensorstate; tracks : Mctypes.ttracksarray; + iffdetectedtracks : Mctypes.tdetectedifftracksarray) +returns (ifftracks : Mctypes.tifftracksarray) +var l34 : Mctypes.ttrack^Mctypes.ksizeifftracksarray; + l40 : Mctypes.tifftracksarray; +let + l34 = + map<> selectdetectedtrack + <()>(iffdetectedtracks, tracks^Mctypes.ksizeifftracksarray, + Mctypes.kinittrack^Mctypes.ksizeifftracksarray); + l40 = map<> ifftrack_of_track<()>(l34); + ifftracks = + if (=)(st, Mctypes.TState_ON) then l40 else Mctypes.kinitifftrackarray +tel + +node iff(tracks : Mctypes.ttracksarray; failure : bool; + iffdetectedtracks : Mctypes.tdetectedifftracksarray; + onoffcmd : bool) +returns (st : Mctypes.tsensorstate; ifftracks : Mctypes.tifftracksarray; + initializing : bool) +var onoffcmd_2 : bool; failure_2 : bool; x : bool; initializing_2 : bool; + st_3 : Mctypes.tsensorstate; st_2 : Mctypes.tsensorstate; + tracks_2 : Mctypes.ttracksarray; + iffdetectedtracks_2 : Mctypes.tdetectedifftracksarray; + l34 : Mctypes.ttrack^Mctypes.ksizeifftracksarray; + l40 : Mctypes.tifftracksarray; ifftracks_2 : Mctypes.tifftracksarray; +let + onoffcmd_2 = onoffcmd; + failure_2 = failure; + initializing_2 = (&)((=)(st_3, Mctypes.TState_OFF), onoffcmd_2); + x = false fby false fby false fby false fby false fby onoffcmd_2; + st_3 = + if failure_2 + then Mctypes.TState_FAIL + else if if onoffcmd_2 then x else false + then Mctypes.TState_ON + else Mctypes.TState_OFF + ; + st_2 = st; + tracks_2 = tracks; + iffdetectedtracks_2 = iffdetectedtracks; + l34 = + map<> selectdetectedtrack + <()>(iffdetectedtracks_2, tracks_2^Mctypes.ksizeifftracksarray, + Mctypes.kinittrack^Mctypes.ksizeifftracksarray); + l40 = map<> ifftrack_of_track<()>(l34); + ifftracks_2 = + if (=)(st_2, Mctypes.TState_ON) then l40 else Mctypes.kinitifftrackarray; + ifftracks = iff_tracks(st, tracks, iffdetectedtracks); + (initializing, st) = iff_state(onoffcmd, failure) +tel + +node advrandr(min : float; max : float) returns (output1 : float) +let + output1 = (+.)((-.)(max, min) *. Mc_ext.rand(), min) +tel + +node advrandi(min : int; max : int; step : int) returns (output1 : int) +var l8 : int; +let + l8 = if not((=)(0, step)) then step else 1; + output1 = + (/) + ((+) + (Mc_ext.int_of_float + (Mc_ext.float_of_int((-)(max, min)) *. Mc_ext.rand()), min), l8 * l8) +tel + +node createtracks_createonetrack_init_rand() +returns (sloperadinit : float; speedinit : float; xmeterinit : float; + ymeterinit : float; idinit : int) +var min : int; max : int; step : int; l8 : int; output1 : int; +let + min = 0; + max = 1000; + step = 10; + l8 = if not((=)(0, step)) then step else 1; + output1 = + (/) + ((+) + (Mc_ext.int_of_float + (Mc_ext.float_of_int((-)(max, min)) *. Mc_ext.rand()), min), l8 * l8); + speedinit = advrandr(250.000000, 1000.000000) *. Mctypes.t; + ymeterinit = Mctypes.nm *. advrandr(~-.(10.000000), 10.000000); + xmeterinit = advrandr(~-.(10.000000), 10.000000) *. Mctypes.nm; + sloperadinit = + (/.) + ((2.000000 *. Mctypes.pi) *. advrandr(0.000000, 360.000000), 360.000000); + idinit = advrandi(0, 1000, 10) +tel + +node createtracks_createonetrack_rand(res : bool) +returns (track : Mctypes.ttrack) +var sloperadinit : float; speedinit : float; xmeterinit : float; + ymeterinit : float; idinit : int; id : int; sloperad : float; + speedt : float; x0 : float; y0 : float; l9 : float; l18 : float; +let + speedinit = advrandr(250.000000, 1000.000000) *. Mctypes.t; + ymeterinit = Mctypes.nm *. advrandr(~-.(10.000000), 10.000000); + xmeterinit = advrandr(~-.(10.000000), 10.000000) *. Mctypes.nm; + sloperadinit = + (/.) + ((2.000000 *. Mctypes.pi) *. advrandr(0.000000, 360.000000), 360.000000); + idinit = advrandi(0, 1000, 10); + (sloperad, speedt, x0, y0, id) = + if res + then createtracks_createonetrack_init_rand() + else (0.000000, 0.000000, 0.000000, 0.000000, 0) fby + (sloperad, speedt, x0, y0, id) + ; + l18 = y0 -> (+.)(Mathext.sinr(sloperad) *. speedt, y0 -> pre l18); + l9 = x0 -> (+.)(x0 -> pre l9, speedt *. Mathext.cosr(sloperad)); + track = + { Mctypes.t_pos = + { Mctypes.x = l9; Mctypes.y = l18 }; + Mctypes.t_id = + id } +tel + +node createtracks_rand(res : bool) returns (tracks : Mctypes.ttracksarray) +let + tracks = + map<> createtracks_createonetrack_rand + <()>(res^Mctypes.ksizetracksarray) +tel + +node createalltracks(res : bool) returns (tracks : Mctypes.ttracksarray) +let + reset tracks = createtracks_rand(res) + every res +tel + +node fusionrdrifftracks(iffmissiontrack : Mctypes.tmissiontrack; + rdrmissiontrack : Mctypes.tmissiontrack) +returns (newiffmissiontrack : Mctypes.tmissiontrack; + newrdrmissiontrack : Mctypes.tmissiontrack) +var pos1 : Mctypes.tposition; pos2 : Mctypes.tposition; v1 : Mctypes.tspeed; + v2 : Mctypes.tspeed; equal : bool; l90 : bool; +let + pos1 = rdrmissiontrack.Mctypes.m_pos; + pos2 = iffmissiontrack.Mctypes.m_pos; + v1 = rdrmissiontrack.Mctypes.m_speed; + v2 = iffmissiontrack.Mctypes.m_speed; + equal = (&)(comparepositions(pos1, pos2), comparespeeds(v1, v2)); + newrdrmissiontrack = + if l90 + then { Mctypes.m_pos = + rdrmissiontrack.Mctypes.m_pos; + Mctypes.m_speed = + rdrmissiontrack.Mctypes.m_speed; + Mctypes.m_id = + iffmissiontrack.Mctypes.m_id; + Mctypes.m_priority = + rdrmissiontrack.Mctypes.m_priority; + Mctypes.m_d = + rdrmissiontrack.Mctypes.m_d; + Mctypes.m_sabs = + rdrmissiontrack.Mctypes.m_sabs; + Mctypes.m_sr = + rdrmissiontrack.Mctypes.m_sr; + Mctypes.m_detectedbyradar = + rdrmissiontrack.Mctypes.m_detectedbyradar; + Mctypes.m_detectedbyiff = + iffmissiontrack.Mctypes.m_detectedbyiff; + Mctypes.m_tracknumber = + 0; + Mctypes.m_targettype = + iffmissiontrack.Mctypes.m_targettype; + Mctypes.m_isvisible = + rdrmissiontrack.Mctypes.m_isvisible; + Mctypes.m_angle = + rdrmissiontrack.Mctypes.m_angle } + else rdrmissiontrack; + l90 = + comparetracks + (rdrmissiontrack.Mctypes.m_pos, iffmissiontrack.Mctypes.m_pos, + rdrmissiontrack.Mctypes.m_speed, iffmissiontrack.Mctypes.m_speed); + newiffmissiontrack = + if l90 then Mctypes.kinitmissiontrack else iffmissiontrack +tel + +node mc_tracks_fusion_onerdrwithifftracks(rdrtrack : Mctypes.tmissiontrack; + ifftracks : Mctypes.tmissiontrack^Mctypes.ksizeifftracksarray) +returns (fusionnedrdrtrack : Mctypes.tmissiontrack; + fusionnedifftracks : Mctypes.tmissiontrack^Mctypes.ksizeifftracksarray) +let + (fusionnedifftracks, fusionnedrdrtrack) = + mapfold<> fusionrdrifftracks + <()>(ifftracks, rdrtrack) +tel + +node mc_tracks_fusion(rdrtracks : Mctypes.trdrtracksarray; + ifftracks : Mctypes.tifftracksarray) +returns (missiontracks : Mctypes.tmissiontracksarray) +var mergedrdrtracks : Mctypes.tmissiontrack^Mctypes.ksizerdrtracksarray; + mergedifftracks : Mctypes.tmissiontrack^Mctypes.ksizeifftracksarray; + l140 : Mctypes.tmissiontrack^Mctypes.ksizerdrtracksarray; + l139 : Mctypes.tmissiontrack^Mctypes.ksizeifftracksarray; +let + missiontracks = mergedrdrtracks @ mergedifftracks; + (mergedrdrtracks, mergedifftracks) = + mapfold<> mc_tracks_fusion_onerdrwithifftracks + <()>(l140, l139); + l140 = + map<> convertrdrtracktomissiontrack + <()>(rdrtracks); + l139 = + map<> convertifftracktomissiontrack + <()>(ifftracks) +tel + +node prio_tracknumbernotinarray(missiontracktracknumber : int; + prioritytrack : int; acc : bool) +returns (notinarray : bool) +let + notinarray = (&)(acc, not((=)(missiontracktracknumber, prioritytrack))) +tel + +node prio_selecthighestprioritynotinpriorityarray(missiontrack : Mctypes.tmissiontrack; + prioritiesarray : Mctypes.tpriorityList; + accprioritymissiontrack : Mctypes.tmissiontrack) +returns (prioritymissiontrack : Mctypes.tmissiontrack) +var missiontracknotinpriorittiesarray : bool; + missiontrackhashigherprioritythanacc : bool; +let + missiontrackhashigherprioritythanacc = + not(trackalowerprioritythanb(missiontrack, accprioritymissiontrack)); + missiontracknotinpriorittiesarray = + fold<<4>> prio_tracknumbernotinarray + <()>(missiontrack.Mctypes.m_tracknumber^4, prioritiesarray, true); + prioritymissiontrack = + if (&) + (missiontracknotinpriorittiesarray, + missiontrackhashigherprioritythanacc) + then missiontrack + else accprioritymissiontrack +tel + +node prio_selectprioritarymissiontracks(missiontracks : Mctypes.tmissiontracksarray; + prioritiesarray : Mctypes.tpriorityList; + indexpriority : int) +returns (newprioritiesarray : Mctypes.tpriorityList) +var missiontrackwithhighestpriority : Mctypes.tmissiontrack; +let + newprioritiesarray = + [prioritiesarray with [indexpriority] = + missiontrackwithhighestpriority.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks, prioritiesarray^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack) +tel + +node prio_setpriorityinmissiontrack(prioritytracknumber : int; + priorityindex : int; + missiontrack : Mctypes.tmissiontrack) +returns (missiontrackwithprio : Mctypes.tmissiontrack) +var missiontrack_2 : Mctypes.tmissiontrack; priority : int; + newmissiontrack : Mctypes.tmissiontrack; +let + missiontrack_2 = missiontrack; + priority = (+)(priorityindex, 1); + newmissiontrack = + {missiontrack_2 with .Mctypes.m_priority = + if missiontrack_2.Mctypes.m_detectedbyradar then priority else 0}; + missiontrackwithprio = + if (=)(prioritytracknumber, missiontrack.Mctypes.m_tracknumber) + then setmissiontrackpriority(missiontrack, (+)(priorityindex, 1)) + else missiontrack +tel + +node prio_setpriorityinmissiontrackarray(priorityarray : Mctypes.tpriorityList; + missiontrack : Mctypes.tmissiontrack) +returns (missiontrackwithprio : Mctypes.tmissiontrack) +let + missiontrackwithprio = + foldi<<4>> prio_setpriorityinmissiontrack + <()>(priorityarray, missiontrack) +tel + +node mc_tracks_prio(missiontracks : Mctypes.tmissiontracksarray) +returns (missiontrackswithprio : Mctypes.tmissiontracksarray) +var missiontracks_2 : Mctypes.tmissiontracksarray; + prioritiesarray : Mctypes.tpriorityList; indexpriority : int; + missiontrackwithhighestpriority : Mctypes.tmissiontrack; + newprioritiesarray : Mctypes.tpriorityList; + prioritytracknumbers : Mctypes.tpriorityList; +let + missiontracks_2 = missiontracks; + prioritiesarray = + prio_selectprioritarymissiontracks + (missiontracks, + prio_selectprioritarymissiontracks + (missiontracks, + prio_selectprioritarymissiontracks(missiontracks, 0^4, 0), 1), + 2); + indexpriority = 3; + newprioritiesarray = + [prioritiesarray with [indexpriority] = + missiontrackwithhighestpriority.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_2, prioritiesarray^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontrackswithprio = + map<> prio_setpriorityinmissiontrackarray + <(prioritytracknumbers)>(missiontracks); + prioritytracknumbers = + prio_selectprioritarymissiontracks + (missiontracks, + prio_selectprioritarymissiontracks + (missiontracks, + prio_selectprioritarymissiontracks + (missiontracks, + prio_selectprioritarymissiontracks(missiontracks, 0^4, 0), 1), + 2), + 3) +tel + +node mc_tracks_tracknumber(withouttracknb : Mctypes.tmissiontracksarray) +returns (withtracknumber : Mctypes.tmissiontracksarray) +var l81 : int; +let + (withtracknumber, l81) = + mapfold<> calculatemissiontracknumber + <(Mctypes.kinitmissiontrackarray -> pre withtracknumber)>(withouttracknb, + 0 -> pre l81) +tel + +node mc_tracks(rdrtracks : Mctypes.trdrtracksarray; + ifftracks : Mctypes.tifftracksarray) +returns (missiontracks : Mctypes.tmissiontracksarray) +var missiontracks_2 : Mctypes.tmissiontracksarray; + prioritytracknumbers : Mctypes.tpriorityList; + missiontrackswithprio : Mctypes.tmissiontracksarray; +let + missiontracks_2 = + mc_tracks_tracknumber(mc_tracks_fusion(rdrtracks, ifftracks)); + missiontrackswithprio = + map<> prio_setpriorityinmissiontrackarray + <(prioritytracknumbers)>(missiontracks_2); + prioritytracknumbers = + prio_selectprioritarymissiontracks + (missiontracks_2, + prio_selectprioritarymissiontracks + (missiontracks_2, + prio_selectprioritarymissiontracks + (missiontracks_2, + prio_selectprioritarymissiontracks(missiontracks_2, 0^4, 0), 1), + 2), + 3); + missiontracks = + mc_tracks_prio + (mc_tracks_tracknumber(mc_tracks_fusion(rdrtracks, ifftracks))) +tel + +node mc(currentrdrstate : Mctypes.tsensorstate; + currentrdrmode : Mctypes.trdrmode; + rdrtracks : Mctypes.trdrtracksarray; rdronoffbutton : bool; + rdrmodebutton : bool; iffonoffbutton : bool; + currentiffstate : Mctypes.tsensorstate; + ifftracks : Mctypes.tifftracksarray) +returns (rdronoffcmd : bool; rdrmodecmd : bool; + missiontracks : Mctypes.tmissiontracksarray; iffonoffcmd : bool) +var rdronoffbutton_2 : bool; currentrdrstate_3 : Mctypes.tsensorstate; + rdronoffcmd_2 : bool; currentrdrstate_2 : Mctypes.tsensorstate; + rdrmodebutton_2 : bool; currentrdrmode_2 : Mctypes.trdrmode; + rdrmodecmd_2 : bool; iffonoffbutton_2 : bool; + currentiffstate_2 : Mctypes.tsensorstate; iffonoffcmd_2 : bool; + rdrtracks_2 : Mctypes.trdrtracksarray; + ifftracks_2 : Mctypes.tifftracksarray; + missiontracks_2 : Mctypes.tmissiontracksarray; +let + rdronoffbutton_2 = rdronoffbutton; + currentrdrstate_3 = currentrdrstate; + rdronoffcmd_2 = statecmd(risingEdge(rdronoffbutton_2), currentrdrstate_3); + currentrdrstate_2 = currentrdrstate; + rdrmodebutton_2 = rdrmodebutton; + currentrdrmode_2 = currentrdrmode; + rdrmodecmd_2 = + rdrmodecmd + (currentrdrstate_2, risingEdge(rdrmodebutton_2), currentrdrmode_2); + iffonoffbutton_2 = iffonoffbutton; + currentiffstate_2 = currentiffstate; + iffonoffcmd_2 = statecmd(risingEdge(iffonoffbutton_2), currentiffstate_2); + rdrtracks_2 = rdrtracks; + ifftracks_2 = ifftracks; + missiontracks_2 = + mc_tracks_prio + (mc_tracks_tracknumber(mc_tracks_fusion(rdrtracks_2, ifftracks_2))); + missiontracks = mc_tracks(rdrtracks, ifftracks); + iffonoffcmd = mc_iffstatecmd(iffonoffbutton, currentiffstate); + rdrmodecmd = mc_rdrmodecmd(currentrdrstate, rdrmodebutton, currentrdrmode); + rdronoffcmd = mc_rdrstatecmd(rdronoffbutton, currentrdrstate) +tel + +node implies(a : bool; b : bool) returns (c : bool) +let + c = (or)(not(a), b) +tel + +node dv_detectedbyiff(missiontrack : Mctypes.tmissiontrack; accin : bool) +returns (accout : bool) +let + accout = (&)(accin, not(not((=)(missiontrack.Mctypes.m_tracknumber, 0)))) +tel + +node dv_sametracknumber(missiontrack1 : Mctypes.tmissiontrack; + missiontrack2 : Mctypes.tmissiontrack; accin : bool) +returns (accout : bool) +let + accout = + (or) + (accin, + (&) + ((=) + (missiontrack1.Mctypes.m_tracknumber, + missiontrack2.Mctypes.m_tracknumber), + not((=)(missiontrack2.Mctypes.m_tracknumber, 0)))) + +tel + +node dv_tracknumberexist(missiontrack : Mctypes.tmissiontrack; + missiontracks : Mctypes.tmissiontracksarray; + accin : bool) +returns (accout : bool) +var l36 : bool; +let + l36 = + fold<> dv_sametracknumber + <()>(missiontrack^Mctypes.ksizemissiontracksarray, missiontracks, + false); + accout = (or)(accin, l36) +tel + +node dv_proof1(currentrdrstate : Mctypes.tsensorstate; rdronoffbutton : bool; + rdronoffcmd : bool) +returns (proof1 : bool) +var a : bool; b : bool; c : bool; +let + a = + (&) + (risingEdge(rdronoffbutton), (=)(currentrdrstate, Mctypes.TState_FAIL)); + b = (=)(rdronoffcmd, false -> pre rdronoffcmd); + c = (or)(not(a), b); + proof1 = + implies + ((&) + (risingEdge(rdronoffbutton), (=)(currentrdrstate, Mctypes.TState_FAIL)), + (=)(rdronoffcmd, false -> pre rdronoffcmd)) +tel + +node dv_proof2(ifftracks : Mctypes.tifftracksarray; + missiontracks : Mctypes.tmissiontracksarray) +returns (proof2 : bool) +var a : bool; b : bool; c : bool; l33 : bool; +let + a = (=)(ifftracks, Mctypes.kinitifftrackarray); + b = l33; + c = (or)(not(a), b); + l33 = + fold<> dv_detectedbyiff + <()>(missiontracks, true); + proof2 = implies((=)(ifftracks, Mctypes.kinitifftrackarray), l33) +tel + +node dv_proof3(missiontracks : Mctypes.tmissiontracksarray) +returns (proof3 : bool) +var l33 : bool; +let + l33 = + fold<> dv_tracknumberexist + <()>(missiontracks, missiontracks^Mctypes.ksizemissiontracksarray, + false); + proof3 = not(l33) +tel + +node dv_observer(currentrdrstate : Mctypes.tsensorstate; + currentrdrmode : Mctypes.trdrmode; + rdrtracks : Mctypes.trdrtracksarray; rdronoffbutton : bool; + rdrmodebutton : bool; iffonoffbutton : bool; + currentiffstate : Mctypes.tsensorstate; + ifftracks : Mctypes.tifftracksarray) +returns (proof1 : bool; proof2 : bool; proof3 : bool) +var currentrdrstate_3 : Mctypes.tsensorstate; + currentrdrmode_2 : Mctypes.trdrmode; + rdrtracks_2 : Mctypes.trdrtracksarray; rdronoffbutton_3 : bool; + rdrmodebutton_2 : bool; iffonoffbutton_2 : bool; + currentiffstate_2 : Mctypes.tsensorstate; + ifftracks_3 : Mctypes.tifftracksarray; rdronoffcmd_2 : bool; + rdrmodecmd : bool; missiontracks_3 : Mctypes.tmissiontracksarray; + iffonoffcmd : bool; currentrdrstate_2 : Mctypes.tsensorstate; + rdronoffbutton_2 : bool; rdronoffcmd : bool; proof1_2 : bool; + ifftracks_2 : Mctypes.tifftracksarray; + missiontracks_2 : Mctypes.tmissiontracksarray; l33_2 : bool; + proof2_2 : bool; missiontracks : Mctypes.tmissiontracksarray; l33 : bool; + proof3_2 : bool; l3 : Mctypes.tmissiontracksarray; l1 : bool; l4 : bool; + l5 : bool; +let + currentrdrstate_3 = currentrdrstate; + currentrdrmode_2 = currentrdrmode; + rdrtracks_2 = rdrtracks; + rdronoffbutton_3 = rdronoffbutton; + rdrmodebutton_2 = rdrmodebutton; + iffonoffbutton_2 = iffonoffbutton; + currentiffstate_2 = currentiffstate; + ifftracks_3 = ifftracks; + missiontracks_3 = mc_tracks(rdrtracks_2, ifftracks_3); + iffonoffcmd = mc_iffstatecmd(iffonoffbutton_2, currentiffstate_2); + rdrmodecmd = + mc_rdrmodecmd(currentrdrstate_3, rdrmodebutton_2, currentrdrmode_2); + rdronoffcmd_2 = mc_rdrstatecmd(rdronoffbutton_3, currentrdrstate_3); + currentrdrstate_2 = currentrdrstate; + rdronoffbutton_2 = rdronoffbutton; + rdronoffcmd = l1; + proof1_2 = + implies + ((&) + (risingEdge(rdronoffbutton_2), + (=)(currentrdrstate_2, Mctypes.TState_FAIL)), + (=)(rdronoffcmd, false -> pre rdronoffcmd)); + ifftracks_2 = ifftracks; + missiontracks_2 = l3; + l33_2 = + fold<> dv_detectedbyiff + <()>(missiontracks_2, true); + proof2_2 = implies((=)(ifftracks_2, Mctypes.kinitifftrackarray), l33_2); + missiontracks = l3; + l33 = + fold<> dv_tracknumberexist + <()>(missiontracks, missiontracks^Mctypes.ksizemissiontracksarray, + false); + proof3_2 = not(l33); + proof3 = dv_proof3(l3); + proof2 = dv_proof2(ifftracks, l3); + proof1 = dv_proof1(currentrdrstate, rdronoffbutton, l1); + (l1, l4, l3, l5) = + mc + (currentrdrstate, currentrdrmode, rdrtracks, rdronoffbutton, + rdrmodebutton, iffonoffbutton, currentiffstate, ifftracks) +tel + +node fighterdebug(res : bool; rdronoffclicked : bool; iffonoffclicked : bool) +returns (missiontracks : Mctypes.tmissiontracksarray) +var onoffcmd_2 : bool; modecmd : bool; failure_2 : bool; + rdrdetectedtracks : Mctypes.tdetectedrdrtracksarray; + tracks_3 : Mctypes.ttracksarray; initializing_2 : bool; + st_2 : Mctypes.tsensorstate; mode : Mctypes.trdrmode; + rdrtracks_2 : Mctypes.trdrtracksarray; tracks_2 : Mctypes.ttracksarray; + failure : bool; iffdetectedtracks : Mctypes.tdetectedifftracksarray; + onoffcmd : bool; st : Mctypes.tsensorstate; + ifftracks_2 : Mctypes.tifftracksarray; initializing : bool; + currentrdrstate : Mctypes.tsensorstate; + currentrdrmode : Mctypes.trdrmode; rdrtracks : Mctypes.trdrtracksarray; + rdronoffbutton : bool; rdrmodebutton : bool; iffonoffbutton : bool; + currentiffstate : Mctypes.tsensorstate; + ifftracks : Mctypes.tifftracksarray; rdronoffcmd : bool; + rdrmodecmd : bool; missiontracks_2 : Mctypes.tmissiontracksarray; + iffonoffcmd : bool; res_2 : bool; tracks : Mctypes.ttracksarray; + l4 : Mctypes.trdrtracksarray; l3 : Mctypes.trdrmode; + l6 : Mctypes.tifftracksarray; l5 : Mctypes.tsensorstate; l12 : bool; + l11 : bool; l10 : bool; l172 : Mctypes.tsensorstate; + l179 : Mctypes.ttracksarray; l200 : bool; l201 : bool; +let + onoffcmd_2 = false -> pre l10; + modecmd = false -> pre l11; + failure_2 = false; + rdrdetectedtracks = [0, 1, 2, 3, 4]; + tracks_3 = l179; + rdrtracks_2 = radar_tracks(st_2, tracks_3, rdrdetectedtracks); + mode = radar_mode(modecmd); + (initializing_2, st_2) = radar_state(onoffcmd_2, failure_2); + tracks_2 = l179; + failure = false; + iffdetectedtracks = [1, 2, 3]; + onoffcmd = false -> pre l12; + ifftracks_2 = iff_tracks(st, tracks_2, iffdetectedtracks); + (initializing, st) = iff_state(onoffcmd, failure); + currentrdrstate = l172; + currentrdrmode = l3; + rdrtracks = l4; + rdronoffbutton = rdronoffclicked; + rdrmodebutton = false; + iffonoffbutton = iffonoffclicked; + currentiffstate = l5; + ifftracks = l6; + missiontracks_2 = mc_tracks(rdrtracks, ifftracks); + iffonoffcmd = mc_iffstatecmd(iffonoffbutton, currentiffstate); + rdrmodecmd = mc_rdrmodecmd(currentrdrstate, rdrmodebutton, currentrdrmode); + rdronoffcmd = mc_rdrstatecmd(rdronoffbutton, currentrdrstate); + res_2 = res; + reset tracks = createtracks_rand(res_2) + every res_2; + l179 = createalltracks(res); + (l10, l11, missiontracks, l12) = + mc(l172, l3, l4, rdronoffclicked, false, iffonoffclicked, l5, l6); + (l5, l6, l200) = iff(l179, false, [1, 2, 3], false -> pre l12); + (l201, l172, l3, l4) = + radar(false -> pre l10, false -> pre l11, false, [0, 1, 2, 3, 4], l179) +tel + +node dv_fighterdebug(res : bool; rdronoffclicked : bool; + iffonoffclicked : bool) +returns (proof3 : bool) +var missiontracks : Mctypes.tmissiontracksarray; l33 : bool; proof3_2 : bool; +let + missiontracks = fighterdebug(res, rdronoffclicked, iffonoffclicked); + l33 = + fold<> dv_tracknumberexist + <()>(missiontracks, missiontracks^Mctypes.ksizemissiontracksarray, + false); + proof3_2 = not(l33); + proof3 = dv_proof3(fighterdebug(res, rdronoffclicked, iffonoffclicked)) +tel + +node dv_debug(missiontracks : Mctypes.tmissiontracksarray) +returns (proof3 : bool) +var missiontracks_2 : Mctypes.tmissiontracksarray; l33 : bool; + proof3_2 : bool; +let + missiontracks_2 = missiontracks; + l33 = + fold<> dv_tracknumberexist + <()>(missiontracks_2, missiontracks_2^Mctypes.ksizemissiontracksarray, + false); + proof3_2 = not(l33); + proof3 = dv_proof3(missiontracks) +tel diff --git a/examples/MC_inlined/mctypes.epi b/examples/MC_inlined/mctypes.epi index c20fcf4..16ee2a6 100644 --- a/examples/MC_inlined/mctypes.epi +++ b/examples/MC_inlined/mctypes.epi @@ -142,3 +142,5 @@ type tpriorityList = int^4 type trdrmode = TRdrMode_WIDE | TRdrMode_NARROW type tsensorstate = TState_OFF | TState_ON | TState_FAIL + +const trackarrayinit:bool = false diff --git a/examples/MC_memalloc/build b/examples/MC_memalloc/build index b1889bc..6c775b7 100755 --- a/examples/MC_memalloc/build +++ b/examples/MC_memalloc/build @@ -1,6 +1,6 @@ #!/bin/bash HEPTC=../../heptc -HEPTC_OPTIONS="" +HEPTC_OPTIONS="-memalloc" GCC=gcc GCC_OPTIONS="-g -O2 -std=c99 -I ../../../lib/c"