From 168a1616902e568bd1ce992a7e8794ce746e30dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Thu, 15 Sep 2011 17:20:49 +0200 Subject: [PATCH] Correct inlined version --- examples/MC_inlined/build | 6 +- examples/MC_inlined/mcinlined.ept | 2059 +++++++++++++++++++++++------ 2 files changed, 1667 insertions(+), 398 deletions(-) diff --git a/examples/MC_inlined/build b/examples/MC_inlined/build index 695b556..90bac3d 100755 --- a/examples/MC_inlined/build +++ b/examples/MC_inlined/build @@ -9,7 +9,7 @@ VERBOSE=1 interfaces=(mctypes.epi) ext_libs=(mc_ext.epi mathext.epi) -sources=() +sources=(mcinlined.ept) for f in ${interfaces[@]}; do if [ $VERBOSE ] ; then @@ -32,9 +32,9 @@ for f in ${sources[@]}; do $HEPTC $HEPTC_OPTIONS -target c $f done -$HEPTC $HEPTC_OPTIONS -target c -s dv_fighterdebug mcinlined.ept +#$HEPTC $HEPTC_OPTIONS -target c -s dv_fighterdebug mcinlined.ept -source_dirs=(mctypes_c mc_c) +source_dirs=(mctypes_c mcinlined_c) other_files=(main.c mathext.c mathext.h mc_ext.c mc_ext.h) if [ -d _build ]; then rm -r _build diff --git a/examples/MC_inlined/mcinlined.ept b/examples/MC_inlined/mcinlined.ept index 321b412..540e3a7 100644 --- a/examples/MC_inlined/mcinlined.ept +++ b/examples/MC_inlined/mcinlined.ept @@ -15,51 +15,61 @@ let tel node myarctan(y : float; x : float) returns (atan : float) -var l6 : float; l4 : bool; l1 : float; +var a_2 : float; o_2 : float; a : float; o : float; l6 : float; l4 : bool; + l1 : float; let + a_2 = x; + o_2 = if (<=.)(0.000000, a_2) then a_2 else ~-.(a_2); + a = y; + o = + if (>.)(a, 0.000000) + then 1.000000 + else if (=)(0.000000, a) then 0.000000 else ~-.(1.000000); atan = if l4 then if (<.)(x, 0.000000) then (+.)(Mctypes.pi, l1) else l1 - else (Mctypes.pi /. 2.000000) *. sign(y); + else (Mctypes.pi /. 2.000000) *. o; l6 = if l4 then (/.)(y, x) else 0.000000 -> pre l6; - l4 = (>.)(abs(x), 0.100000); + l4 = (>.)(o_2, 0.100000); l1 = Mathext.atanr(l6) tel node missiontrackequalsprevious(previousone : Mctypes.tmissiontrack; actualone : Mctypes.tmissiontrack) returns (equal : bool) +var a_6 : float; o_6 : float; a_5 : float; o_5 : float; a_4 : float; + o_4 : float; a_3 : float; o_3 : float; a_2 : float; o_2 : float; + a : float; o : float; let + a_6 = actualone.Mctypes.m_pos.Mctypes.y; + o_6 = if (<=.)(0.000000, a_6) then a_6 else ~-.(a_6); + a_5 = actualone.Mctypes.m_pos.Mctypes.x; + o_5 = if (<=.)(0.000000, a_5) then a_5 else ~-.(a_5); + a_4 = previousone.Mctypes.m_pos.Mctypes.y; + o_4 = if (<=.)(0.000000, a_4) then a_4 else ~-.(a_4); + a_3 = previousone.Mctypes.m_pos.Mctypes.x; + o_3 = if (<=.)(0.000000, a_3) then a_3 else ~-.(a_3); + a_2 = + (-.) + (previousone.Mctypes.m_pos.Mctypes.y, actualone.Mctypes.m_pos.Mctypes.y); + o_2 = if (<=.)(0.000000, a_2) then a_2 else ~-.(a_2); + a = + (-.) + (previousone.Mctypes.m_pos.Mctypes.x, actualone.Mctypes.m_pos.Mctypes.x); + o = if (<=.)(0.000000, a) then a else ~-.(a); 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)) - , + ((&)((<.)(o, 100.000000), (<.)(o_2, 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))) + ((&)((<.)(o_3, 0.100000), (<.)(o_4, 0.100000)), + (<.)(o_5, 0.100000)), + (<.)(o_6, 0.100000))) ) ) @@ -67,16 +77,22 @@ tel node calctrackvisible1(position : Mctypes.tposition; speed : Mctypes.tspeed) returns (trackvisible : bool) +var a_4 : float; o_4 : float; a_3 : float; o_3 : float; a_2 : float; + o_2 : float; a : float; o : float; let + a_4 = speed.Mctypes.sy; + o_4 = if (<=.)(0.000000, a_4) then a_4 else ~-.(a_4); + a_3 = speed.Mctypes.sx; + o_3 = if (<=.)(0.000000, a_3) then a_3 else ~-.(a_3); + a_2 = position.Mctypes.y; + o_2 = if (<=.)(0.000000, a_2) then a_2 else ~-.(a_2); + a = position.Mctypes.x; + o = if (<=.)(0.000000, a) then a else ~-.(a); 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))) + ((&)((&)((<.)(o, 0.001000), (<.)(o_2, 0.001000)), (<.)(o_3, 0.001000)), + (<.)(o_4, 0.001000))) tel @@ -84,11 +100,47 @@ node missiontrackexist1(acc_tracknumber : int; missiontrack : Mctypes.tmissiontrack; previousmissiontrack : Mctypes.tmissiontrack) returns (tracknumbertoset : int) +var previousone : Mctypes.tmissiontrack; actualone : Mctypes.tmissiontrack; + a_6 : float; o_6 : float; a_5 : float; o_5 : float; a_4 : float; + o_4 : float; a_3 : float; o_3 : float; a_2 : float; o_2 : float; + a : float; o : float; equal : bool; let + previousone = missiontrack; + actualone = previousmissiontrack; + a_6 = actualone.Mctypes.m_pos.Mctypes.y; + o_6 = if (<=.)(0.000000, a_6) then a_6 else ~-.(a_6); + a_5 = actualone.Mctypes.m_pos.Mctypes.x; + o_5 = if (<=.)(0.000000, a_5) then a_5 else ~-.(a_5); + a_4 = previousone.Mctypes.m_pos.Mctypes.y; + o_4 = if (<=.)(0.000000, a_4) then a_4 else ~-.(a_4); + a_3 = previousone.Mctypes.m_pos.Mctypes.x; + o_3 = if (<=.)(0.000000, a_3) then a_3 else ~-.(a_3); + a_2 = + (-.) + (previousone.Mctypes.m_pos.Mctypes.y, actualone.Mctypes.m_pos.Mctypes.y); + o_2 = if (<=.)(0.000000, a_2) then a_2 else ~-.(a_2); + a = + (-.) + (previousone.Mctypes.m_pos.Mctypes.x, actualone.Mctypes.m_pos.Mctypes.x); + o = if (<=.)(0.000000, a) then a else ~-.(a); + equal = + (or) + ((&) + (not((=)(0, previousone.Mctypes.m_id)), + (=)(previousone.Mctypes.m_id, actualone.Mctypes.m_id)), + (&) + ((&)((<.)(o, 100.000000), (<.)(o_2, 100.000000)), + not + ((&) + ((&) + ((&)((<.)(o_3, 0.100000), (<.)(o_4, 0.100000)), + (<.)(o_5, 0.100000)), + (<.)(o_6, 0.100000))) + ) + ) + ; tracknumbertoset = - if (&) - (missiontrackequalsprevious(missiontrack, previousmissiontrack), - not((=)(0, previousmissiontrack.Mctypes.m_tracknumber))) + if (&)(equal, not((=)(0, previousmissiontrack.Mctypes.m_tracknumber))) then previousmissiontrack.Mctypes.m_tracknumber else acc_tracknumber tel @@ -96,8 +148,26 @@ tel node missiontrackequalsprevious_orig(previousone : Mctypes.tmissiontrack; actualone : Mctypes.tmissiontrack) returns (equal : bool) -var l43 : bool; +var a_6 : float; o_6 : float; a_5 : float; o_5 : float; a_4 : float; + o_4 : float; a_3 : float; o_3 : float; a_2 : float; o_2 : float; + a : float; o : float; l43 : bool; let + a_6 = actualone.Mctypes.m_pos.Mctypes.y; + o_6 = if (<=.)(0.000000, a_6) then a_6 else ~-.(a_6); + a_5 = actualone.Mctypes.m_pos.Mctypes.x; + o_5 = if (<=.)(0.000000, a_5) then a_5 else ~-.(a_5); + a_4 = previousone.Mctypes.m_pos.Mctypes.y; + o_4 = if (<=.)(0.000000, a_4) then a_4 else ~-.(a_4); + a_3 = previousone.Mctypes.m_pos.Mctypes.x; + o_3 = if (<=.)(0.000000, a_3) then a_3 else ~-.(a_3); + a_2 = + (-.) + (previousone.Mctypes.m_pos.Mctypes.y, actualone.Mctypes.m_pos.Mctypes.y); + o_2 = if (<=.)(0.000000, a_2) then a_2 else ~-.(a_2); + a = + (-.) + (previousone.Mctypes.m_pos.Mctypes.x, actualone.Mctypes.m_pos.Mctypes.x); + o = if (<=.)(0.000000, a) then a else ~-.(a); l43 = not((=)(previousone.Mctypes.m_tracknumber, 0)); equal = (&) @@ -107,30 +177,13 @@ let ((&)(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)) - , + ((&)((<.)(o, 100.000000), (<.)(o_2, 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))) + ((&)((<.)(o_3, 0.100000), (<.)(o_4, 0.100000)), + (<.)(o_5, 0.100000)), + (<.)(o_6, 0.100000))) ) ) ) @@ -150,34 +203,37 @@ tel node calctrackangle(speed : Mctypes.tspeed; speedabs : Mctypes.tmetresseconde) returns (trackangle : float) -var a : float; o : float; l51 : bool; l48 : float; l47 : float; +var a_2 : float; o_2 : float; a : float; o : float; input1 : float; + output1 : float; l51 : bool; l48 : float; l47 : float; let - a = l47; + a_2 = l47; + o_2 = + if (>.)(a_2, 0.000000) + then 1.000000 + else if (=)(0.000000, a_2) then 0.000000 else ~-.(1.000000); + a = + Mathext.asinr((/.)(speed.Mctypes.sy, if l51 then 1.000000 else speedabs)); 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))) - ; + input1 = if l51 then 0.000000 else Mathext.acosr(l47) *. l48; + output1 = (/.)(input1, (2.000000 *. Mctypes.pi)) *. 360.000000; + trackangle = output1 *. l48 *. o; l51 = (<.)(speedabs, 0.010000); - l48 = sign(l47); + l48 = o_2; l47 = (/.)(speed.Mctypes.sx, if l51 then 1.000000 else speedabs) tel node calctrackvisible(position : Mctypes.tposition) returns (trackvisible : bool) +var a_2 : float; o_2 : float; a : float; o : float; let - trackvisible = - not - ((&) - ((<.)(abs(position.Mctypes.x), 0.001000), - (<.)(abs(position.Mctypes.y), 0.001000))) - + a_2 = position.Mctypes.y; + o_2 = if (<=.)(0.000000, a_2) then a_2 else ~-.(a_2); + a = position.Mctypes.x; + o = if (<=.)(0.000000, a) then a else ~-.(a); + trackvisible = not((&)((<.)(o, 0.001000), (<.)(o_2, 0.001000))) tel node missiontrackexist(missiontrack : Mctypes.tmissiontrack; @@ -185,45 +241,46 @@ node missiontrackexist(missiontrack : Mctypes.tmissiontrack; acc_tracknumber : int) returns (tracknumbertoset : int) var previousone : Mctypes.tmissiontrack; actualone : Mctypes.tmissiontrack; - equal : bool; + a_6 : float; o_6 : float; a_5 : float; o_5 : float; a_4 : float; + o_4 : float; a_3 : float; o_3 : float; a_2 : float; o_2 : float; + a : float; o : float; equal : bool; let previousone = missiontrack; actualone = previousmissiontrack; + a_6 = actualone.Mctypes.m_pos.Mctypes.y; + o_6 = if (<=.)(0.000000, a_6) then a_6 else ~-.(a_6); + a_5 = actualone.Mctypes.m_pos.Mctypes.x; + o_5 = if (<=.)(0.000000, a_5) then a_5 else ~-.(a_5); + a_4 = previousone.Mctypes.m_pos.Mctypes.y; + o_4 = if (<=.)(0.000000, a_4) then a_4 else ~-.(a_4); + a_3 = previousone.Mctypes.m_pos.Mctypes.x; + o_3 = if (<=.)(0.000000, a_3) then a_3 else ~-.(a_3); + a_2 = + (-.) + (previousone.Mctypes.m_pos.Mctypes.y, actualone.Mctypes.m_pos.Mctypes.y); + o_2 = if (<=.)(0.000000, a_2) then a_2 else ~-.(a_2); + a = + (-.) + (previousone.Mctypes.m_pos.Mctypes.x, actualone.Mctypes.m_pos.Mctypes.x); + o = if (<=.)(0.000000, a) then a else ~-.(a); 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)) - , + ((&)((<.)(o, 100.000000), (<.)(o_2, 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))) + ((&)((<.)(o_3, 0.100000), (<.)(o_4, 0.100000)), + (<.)(o_5, 0.100000)), + (<.)(o_6, 0.100000))) ) ) ; tracknumbertoset = - if missiontrackequalsprevious(missiontrack, previousmissiontrack) + if equal then previousmissiontrack.Mctypes.m_tracknumber else acc_tracknumber tel @@ -239,30 +296,39 @@ tel node trackalowerprioritythanb(a : Mctypes.tmissiontrack; b : Mctypes.tmissiontrack) returns (prioritary : bool) +var vr_2 : float; d_2 : float; l13_2 : float; l11_2 : bool; result_2 : float; + vr : float; d : float; l13 : float; l11 : bool; result : float; let + vr_2 = b.Mctypes.m_sr; + d_2 = b.Mctypes.m_d; + result_2 = if l11_2 then l13_2 else 0.000000; + l13_2 = if l11_2 then (/.)(vr_2, d_2) else 0.000000 -> pre l13_2; + l11_2 = (>.)(d_2, 0.100000); + vr = a.Mctypes.m_sr; + d = a.Mctypes.m_d; + result = if l11 then l13 else 0.000000; + l13 = if l11 then (/.)(vr, d) else 0.000000 -> pre l13; + l11 = (>.)(d, 0.100000); 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))) - , + ((&)(a.Mctypes.m_detectedbyradar, (<.)(result, result_2)), b.Mctypes.m_detectedbyradar)) tel node comparespeeds(speed1 : Mctypes.tspeed; speed2 : Mctypes.tspeed) returns (equal : bool) +var a_2 : float; o_2 : float; a : float; o : float; let - equal = - (&) - ((<.)(abs((-.)(speed1.Mctypes.sx, speed2.Mctypes.sx)), 1.000000), - (<.)(abs((-.)(speed1.Mctypes.sy, speed2.Mctypes.sy)), 1.000000)) + a_2 = (-.)(speed1.Mctypes.sy, speed2.Mctypes.sy); + o_2 = if (<=.)(0.000000, a_2) then a_2 else ~-.(a_2); + a = (-.)(speed1.Mctypes.sx, speed2.Mctypes.sx); + o = if (<=.)(0.000000, a) then a else ~-.(a); + equal = (&)((<.)(o, 1.000000), (<.)(o_2, 1.000000)) tel node calculateprioritizedtracknb(missiontrack : Mctypes.tmissiontrack) @@ -287,18 +353,38 @@ tel node comparepositions(pos1 : Mctypes.tposition; pos2 : Mctypes.tposition) returns (equal : bool) +var a_2 : float; o_2 : float; a : float; o : float; let - equal = - (&) - ((<.)(abs((-.)(pos1.Mctypes.x, pos2.Mctypes.x)), 0.100000), - (<.)(abs((-.)(pos1.Mctypes.y, pos2.Mctypes.y)), 0.100000)) + a_2 = (-.)(pos1.Mctypes.y, pos2.Mctypes.y); + o_2 = if (<=.)(0.000000, a_2) then a_2 else ~-.(a_2); + a = (-.)(pos1.Mctypes.x, pos2.Mctypes.x); + o = if (<=.)(0.000000, a) then a else ~-.(a); + equal = (&)((<.)(o, 0.100000), (<.)(o_2, 0.100000)) tel node comparetracks(pos1 : Mctypes.tposition; pos2 : Mctypes.tposition; v1 : Mctypes.tspeed; v2 : Mctypes.tspeed) returns (equal : bool) +var speed1 : Mctypes.tspeed; speed2 : Mctypes.tspeed; a_2_2 : float; + o_2_2 : float; a_3 : float; o_3 : float; equal_3 : bool; + pos1_2 : Mctypes.tposition; pos2_2 : Mctypes.tposition; a_2 : float; + o_2 : float; a : float; o : float; equal_2 : bool; let - equal = (&)(comparepositions(pos1, pos2), comparespeeds(v1, v2)) + speed1 = v1; + speed2 = v2; + a_2_2 = (-.)(speed1.Mctypes.sy, speed2.Mctypes.sy); + o_2_2 = if (<=.)(0.000000, a_2_2) then a_2_2 else ~-.(a_2_2); + a_3 = (-.)(speed1.Mctypes.sx, speed2.Mctypes.sx); + o_3 = if (<=.)(0.000000, a_3) then a_3 else ~-.(a_3); + equal_3 = (&)((<.)(o_3, 1.000000), (<.)(o_2_2, 1.000000)); + pos1_2 = pos1; + pos2_2 = pos2; + a_2 = (-.)(pos1_2.Mctypes.y, pos2_2.Mctypes.y); + o_2 = if (<=.)(0.000000, a_2) then a_2 else ~-.(a_2); + a = (-.)(pos1_2.Mctypes.x, pos2_2.Mctypes.x); + o = if (<=.)(0.000000, a) then a else ~-.(a); + equal_2 = (&)((<.)(o, 0.100000), (<.)(o_2, 0.100000)); + equal = (&)(equal_2, equal_3) tel node setmissiontracknumber(missiontrack : Mctypes.tmissiontrack; @@ -311,32 +397,72 @@ tel node missiontrackisnull(missiontrack : Mctypes.tmissiontrack) returns (isnull : bool) var pos1 : Mctypes.tposition; pos2 : Mctypes.tposition; v1 : Mctypes.tspeed; - v2 : Mctypes.tspeed; equal : bool; + v2 : Mctypes.tspeed; speed1 : Mctypes.tspeed; speed2 : Mctypes.tspeed; + a_2_2 : float; o_2_2 : float; a_3 : float; o_3 : float; equal_3 : bool; + pos1_2 : Mctypes.tposition; pos2_2 : Mctypes.tposition; a_2 : float; + o_2 : float; a : float; o : float; equal_2 : bool; 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) + speed1 = v1; + speed2 = v2; + a_2_2 = (-.)(speed1.Mctypes.sy, speed2.Mctypes.sy); + o_2_2 = if (<=.)(0.000000, a_2_2) then a_2_2 else ~-.(a_2_2); + a_3 = (-.)(speed1.Mctypes.sx, speed2.Mctypes.sx); + o_3 = if (<=.)(0.000000, a_3) then a_3 else ~-.(a_3); + equal_3 = (&)((<.)(o_3, 1.000000), (<.)(o_2_2, 1.000000)); + pos1_2 = pos1; + pos2_2 = pos2; + a_2 = (-.)(pos1_2.Mctypes.y, pos2_2.Mctypes.y); + o_2 = if (<=.)(0.000000, a_2) then a_2 else ~-.(a_2); + a = (-.)(pos1_2.Mctypes.x, pos2_2.Mctypes.x); + o = if (<=.)(0.000000, a) then a else ~-.(a); + equal_2 = (&)((<.)(o, 0.100000), (<.)(o_2, 0.100000)); + equal = (&)(equal_2, equal_3); + isnull = equal 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; +var missiontrack_3 : Mctypes.tmissiontrack; number : int; + newmissiontrack_2 : Mctypes.tmissiontrack; + missiontrack_2 : Mctypes.tmissiontrack; pos1 : Mctypes.tposition; + pos2 : Mctypes.tposition; v1 : Mctypes.tspeed; v2 : Mctypes.tspeed; + speed1 : Mctypes.tspeed; speed2 : Mctypes.tspeed; a_2_2 : float; + o_2_2 : float; a_3 : float; o_3 : float; equal_3 : bool; + pos1_2 : Mctypes.tposition; pos2_2 : Mctypes.tposition; a_2 : float; + o_2 : float; a : float; o : float; equal_2 : bool; equal : bool; + isnull : bool; setnewtracknumber : bool; previoustracknumber : int; let - missiontrack_2 = missiontrack; + missiontrack_3 = missiontrack; number = if setnewtracknumber then newtracknumber else previoustracknumber; - newmissiontrack_2 = {missiontrack_2 with .Mctypes.m_tracknumber = number}; - setnewtracknumber = - (&)((=)(previoustracknumber, 0), not(missiontrackisnull(missiontrack))); + newmissiontrack_2 = {missiontrack_3 with .Mctypes.m_tracknumber = number}; + missiontrack_2 = missiontrack; + pos1 = missiontrack_2.Mctypes.m_pos; + pos2 = Mctypes.kInitPosition; + v1 = missiontrack_2.Mctypes.m_speed; + v2 = Mctypes.kInitSpeed; + speed1 = v1; + speed2 = v2; + a_2_2 = (-.)(speed1.Mctypes.sy, speed2.Mctypes.sy); + o_2_2 = if (<=.)(0.000000, a_2_2) then a_2_2 else ~-.(a_2_2); + a_3 = (-.)(speed1.Mctypes.sx, speed2.Mctypes.sx); + o_3 = if (<=.)(0.000000, a_3) then a_3 else ~-.(a_3); + equal_3 = (&)((<.)(o_3, 1.000000), (<.)(o_2_2, 1.000000)); + pos1_2 = pos1; + pos2_2 = pos2; + a_2 = (-.)(pos1_2.Mctypes.y, pos2_2.Mctypes.y); + o_2 = if (<=.)(0.000000, a_2) then a_2 else ~-.(a_2); + a = (-.)(pos1_2.Mctypes.x, pos2_2.Mctypes.x); + o = if (<=.)(0.000000, a) then a else ~-.(a); + equal_2 = (&)((<.)(o, 0.100000), (<.)(o_2, 0.100000)); + equal = (&)(equal_2, equal_3); + isnull = equal; + setnewtracknumber = (&)((=)(previoustracknumber, 0), not(isnull)); newtracknumber = if setnewtracknumber then (+)(currenttracknumber, 1) @@ -344,10 +470,7 @@ let previoustracknumber = fold<> missiontrackexist <(missiontrack)>(previousmissiontracks, 0); - newmissiontrack = - setmissiontracknumber - (missiontrack, - if setnewtracknumber then newtracknumber else previoustracknumber) + newmissiontrack = newmissiontrack_2 tel node calculatetracktargettypefromid(id : int) @@ -363,39 +486,49 @@ let tel node myderivative(inv : float; period : float) returns (o : float) -var l2 : float; +var a_2 : float; o_3 : float; a : float; o_2 : float; l2 : float; let + a_2 = inv; + o_3 = if (<=.)(0.000000, a_2) then a_2 else ~-.(a_2); + a = l2; + o_2 = if (<=.)(0.000000, a) then a else ~-.(a); l2 = 0.000000 fby 0.000000 fby inv; o = - if (or)((<.)(abs(l2), 0.100000), (<.)(abs(inv), 0.100000)) + if (or)((<.)(o_2, 0.100000), (<.)(o_3, 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; +var inv_2 : float; period_2 : float; a_2_2 : float; o_3_2 : float; + a_3 : float; o_2_2 : float; l2_2 : float; o_4 : float; inv : float; + period : float; a_2 : float; o_3 : float; a : float; o_2 : float; + l2 : float; o : float; let inv_2 = position.Mctypes.y; period_2 = Mctypes.t; + a_2_2 = inv_2; + o_3_2 = if (<=.)(0.000000, a_2_2) then a_2_2 else ~-.(a_2_2); + a_3 = l2_2; + o_2_2 = if (<=.)(0.000000, a_3) then a_3 else ~-.(a_3); l2_2 = 0.000000 fby 0.000000 fby inv_2; - o_2 = - if (or)((<.)(abs(l2_2), 0.100000), (<.)(abs(inv_2), 0.100000)) + o_4 = + if (or)((<.)(o_2_2, 0.100000), (<.)(o_3_2, 0.100000)) then 0.000000 else 0.000000 -> (/.)((-.)(inv_2, l2_2), 2.000000 *. period_2); inv = position.Mctypes.x; period = Mctypes.t; + a_2 = inv; + o_3 = if (<=.)(0.000000, a_2) then a_2 else ~-.(a_2); + a = l2; + o_2 = if (<=.)(0.000000, a) then a else ~-.(a); l2 = 0.000000 fby 0.000000 fby inv; o = - if (or)((<.)(abs(l2), 0.100000), (<.)(abs(inv), 0.100000)) + if (or)((<.)(o_2, 0.100000), (<.)(o_3, 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) } + speed = { Mctypes.sx = o; Mctypes.sy = o_4 } tel node selectdetectedtrack(index : int; tracks : Mctypes.ttracksarray; @@ -417,14 +550,36 @@ tel node sortblockmissiontrack(a : Mctypes.tmissiontrack; b : Mctypes.tmissiontrack) returns (newa : Mctypes.tmissiontrack; newb : Mctypes.tmissiontrack) -var missiontrack : Mctypes.tmissiontrack; isnull : bool; l7 : bool; +var missiontrack : Mctypes.tmissiontrack; pos1 : Mctypes.tposition; + pos2 : Mctypes.tposition; v1 : Mctypes.tspeed; v2 : Mctypes.tspeed; + speed1 : Mctypes.tspeed; speed2 : Mctypes.tspeed; a_2_2 : float; + o_2_2 : float; a_3 : float; o_3 : float; equal_3 : bool; + pos1_2 : Mctypes.tposition; pos2_2 : Mctypes.tposition; a_2 : float; + o_2 : float; a_4 : float; o : float; equal_2 : bool; equal : bool; + isnull : bool; l7 : bool; let missiontrack = a; - isnull = - comparetracks - (missiontrack.Mctypes.m_pos, Mctypes.kInitPosition, - missiontrack.Mctypes.m_speed, Mctypes.kInitSpeed); - l7 = missiontrackisnull(a); + pos1 = missiontrack.Mctypes.m_pos; + pos2 = Mctypes.kInitPosition; + v1 = missiontrack.Mctypes.m_speed; + v2 = Mctypes.kInitSpeed; + speed1 = v1; + speed2 = v2; + a_2_2 = (-.)(speed1.Mctypes.sy, speed2.Mctypes.sy); + o_2_2 = if (<=.)(0.000000, a_2_2) then a_2_2 else ~-.(a_2_2); + a_3 = (-.)(speed1.Mctypes.sx, speed2.Mctypes.sx); + o_3 = if (<=.)(0.000000, a_3) then a_3 else ~-.(a_3); + equal_3 = (&)((<.)(o_3, 1.000000), (<.)(o_2_2, 1.000000)); + pos1_2 = pos1; + pos2_2 = pos2; + a_2 = (-.)(pos1_2.Mctypes.y, pos2_2.Mctypes.y); + o_2 = if (<=.)(0.000000, a_2) then a_2 else ~-.(a_2); + a_4 = (-.)(pos1_2.Mctypes.x, pos2_2.Mctypes.x); + o = if (<=.)(0.000000, a_4) then a_4 else ~-.(a_4); + equal_2 = (&)((<.)(o, 0.100000), (<.)(o_2, 0.100000)); + equal = (&)(equal_2, equal_3); + isnull = equal; + l7 = isnull; newb = if l7 then a else b; newa = if l7 then b else a tel @@ -432,26 +587,33 @@ 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; +var a_2 : Mctypes.tmissiontrack; b_2 : Mctypes.tmissiontrack; vr_2 : float; + d_2 : float; l13_2 : float; l11_2 : bool; result_2 : float; vr : float; + d : float; l13 : float; l11 : bool; result : float; prioritary : bool; + l25 : bool; let a_2 = a; b_2 = b; + vr_2 = b_2.Mctypes.m_sr; + d_2 = b_2.Mctypes.m_d; + result_2 = if l11_2 then l13_2 else 0.000000; + l13_2 = if l11_2 then (/.)(vr_2, d_2) else 0.000000 -> pre l13_2; + l11_2 = (>.)(d_2, 0.100000); + vr = a_2.Mctypes.m_sr; + d = a_2.Mctypes.m_d; + result = if l11 then l13 else 0.000000; + l13 = if l11 then (/.)(vr, d) else 0.000000 -> pre l13; + l11 = (>.)(d, 0.100000); 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))) - , + ((&)(a_2.Mctypes.m_detectedbyradar, (<.)(result, result_2)), b_2.Mctypes.m_detectedbyradar)) ; - l25 = trackalowerprioritythanb(a, b); + l25 = prioritary; newb = if l25 then a else b; newa = if l25 then b else a tel @@ -471,18 +633,22 @@ 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; +var position_2 : Mctypes.tposition; a_2_3 : float; o_2_3 : float; + a_4 : float; o_5 : float; trackvisible : bool; id : int; + targettype : Mctypes.ttargettype; p1_2 : Mctypes.tposition; + p2_2 : Mctypes.tposition; res_2 : bool; position : Mctypes.tposition; + inv_2 : float; period_2 : float; a_2_2 : float; o_3_2 : float; + a_3 : float; o_2_2 : float; l2_2 : float; o_4 : float; inv : float; + period : float; a_2 : float; o_3 : float; a : float; o_2 : float; + l2 : float; o : float; 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))) - ; + a_2_3 = position_2.Mctypes.y; + o_2_3 = if (<=.)(0.000000, a_2_3) then a_2_3 else ~-.(a_2_3); + a_4 = position_2.Mctypes.x; + o_5 = if (<=.)(0.000000, a_4) then a_4 else ~-.(a_4); + trackvisible = not((&)((<.)(o_5, 0.001000), (<.)(o_2_3, 0.001000))); id = ifftrack.Mctypes.i_id; targettype = if (=)(0, id) @@ -491,12 +657,36 @@ let then Mctypes.Ttargettype_friend else Mctypes.Ttargettype_foe ; + p1_2 = ifftrack.Mctypes.i_pos; + p2_2 = Mctypes.kInitPosition; + res_2 = + (&) + ((=)(p1_2.Mctypes.x, p2_2.Mctypes.x), + (=)(p1_2.Mctypes.y, p2_2.Mctypes.y)); position = ifftrack.Mctypes.i_pos; - speed = - { Mctypes.sx = - myderivative(position.Mctypes.x, Mctypes.t); - Mctypes.sy = - myderivative(position.Mctypes.y, Mctypes.t) }; + inv_2 = position.Mctypes.y; + period_2 = Mctypes.t; + a_2_2 = inv_2; + o_3_2 = if (<=.)(0.000000, a_2_2) then a_2_2 else ~-.(a_2_2); + a_3 = l2_2; + o_2_2 = if (<=.)(0.000000, a_3) then a_3 else ~-.(a_3); + l2_2 = 0.000000 fby 0.000000 fby inv_2; + o_4 = + if (or)((<.)(o_2_2, 0.100000), (<.)(o_3_2, 0.100000)) + then 0.000000 + else 0.000000 -> (/.)((-.)(inv_2, l2_2), 2.000000 *. period_2); + inv = position.Mctypes.x; + period = Mctypes.t; + a_2 = inv; + o_3 = if (<=.)(0.000000, a_2) then a_2 else ~-.(a_2); + a = l2; + o_2 = if (<=.)(0.000000, a) then a else ~-.(a); + l2 = 0.000000 fby 0.000000 fby inv; + o = + if (or)((<.)(o_2, 0.100000), (<.)(o_3, 0.100000)) + then 0.000000 + else 0.000000 -> (/.)((-.)(inv, l2), 2.000000 *. period); + speed = { Mctypes.sx = o; Mctypes.sy = o_4 }; p1 = Mctypes.kInitPosition; p2 = ifftrack.Mctypes.i_pos; res = (&)((=)(p1.Mctypes.x, p2.Mctypes.x), (=)(p1.Mctypes.y, p2.Mctypes.y)); @@ -504,9 +694,7 @@ let { 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); + if res then Mctypes.kInitSpeed else speed; Mctypes.m_id = ifftrack.Mctypes.i_id; Mctypes.m_priority = @@ -520,46 +708,58 @@ let Mctypes.m_detectedbyradar = false; Mctypes.m_detectedbyiff = - not - ((&) - (position_equal(ifftrack.Mctypes.i_pos, Mctypes.kInitPosition), - (=)(ifftrack.Mctypes.i_id, 0))) - ; + not((&)(res_2, (=)(ifftrack.Mctypes.i_id, 0))); Mctypes.m_tracknumber = 0; Mctypes.m_targettype = - calculatetracktargettypefromid(ifftrack.Mctypes.i_id); + targettype; Mctypes.m_isvisible = - calctrackvisible(ifftrack.Mctypes.i_pos); + trackvisible; 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; +var speed : Mctypes.tspeed; speedabs : Mctypes.tmetresseconde; a_2_2 : float; + o_2_2 : float; a_3 : float; o_3 : float; input1 : float; output1 : float; + l51 : bool; l48 : float; l47 : float; trackangle : float; + position : Mctypes.tposition; a_2 : float; o_2 : float; a : float; + o : float; trackvisible : bool; s1 : Mctypes.tspeed; s2 : Mctypes.tspeed; + res_2 : bool; p1 : Mctypes.tposition; p2 : Mctypes.tposition; res : 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))) - ; + a_2_2 = l47; + o_2_2 = + if (>.)(a_2_2, 0.000000) + then 1.000000 + else if (=)(0.000000, a_2_2) then 0.000000 else ~-.(1.000000); + a_3 = + Mathext.asinr((/.)(speed.Mctypes.sy, if l51 then 1.000000 else speedabs)); + o_3 = + if (>.)(a_3, 0.000000) + then 1.000000 + else if (=)(0.000000, a_3) then 0.000000 else ~-.(1.000000); + input1 = if l51 then 0.000000 else Mathext.acosr(l47) *. l48; + output1 = (/.)(input1, (2.000000 *. Mctypes.pi)) *. 360.000000; + trackangle = output1 *. l48 *. o_3; l51 = (<.)(speedabs, 0.010000); - l48 = sign(l47); + l48 = o_2_2; 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))) - ; + a_2 = position.Mctypes.y; + o_2 = if (<=.)(0.000000, a_2) then a_2 else ~-.(a_2); + a = position.Mctypes.x; + o = if (<=.)(0.000000, a) then a else ~-.(a); + trackvisible = not((&)((<.)(o, 0.001000), (<.)(o_2, 0.001000))); + s1 = rdrtrack.Mctypes.r_s; + s2 = Mctypes.kInitSpeed; + res_2 = + (&)((=)(s1.Mctypes.sx, s2.Mctypes.sx), (=)(s1.Mctypes.sy, s2.Mctypes.sy)); + p1 = rdrtrack.Mctypes.r_pos; + p2 = Mctypes.kInitPosition; + res = (&)((=)(p1.Mctypes.x, p2.Mctypes.x), (=)(p1.Mctypes.y, p2.Mctypes.y)); missiontrack = { Mctypes.m_pos = rdrtrack.Mctypes.r_pos; @@ -579,11 +779,7 @@ let not ((&) ((&) - ((&) - ((&) - (position_equal(rdrtrack.Mctypes.r_pos, Mctypes.kInitPosition), - speed_equal(rdrtrack.Mctypes.r_s, Mctypes.kInitSpeed)), - (=)(rdrtrack.Mctypes.r_d, 0.000000)), + ((&)((&)(res, res_2), (=)(rdrtrack.Mctypes.r_d, 0.000000)), (=)(rdrtrack.Mctypes.r_sabs, 0.000000)), (=)(rdrtrack.Mctypes.r_sr, 0.000000))) ; @@ -594,9 +790,9 @@ let Mctypes.m_targettype = Mctypes.Ttargettype_unknown; Mctypes.m_isvisible = - calctrackvisible(rdrtrack.Mctypes.r_pos); + trackvisible; Mctypes.m_angle = - calctrackangle(rdrtrack.Mctypes.r_s, rdrtrack.Mctypes.r_sabs) } + trackangle } tel node vectnorme(a : float; b : float) returns (c : float) @@ -613,18 +809,39 @@ 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; +var position : Mctypes.tposition; inv_2 : float; period_2 : float; + a_2_2 : float; o_3_2 : float; a_3 : float; o_2_2 : float; l2_2 : float; + o_4 : float; inv : float; period : float; a_2_3 : float; o_3 : float; + a_4 : float; o_2 : float; l2 : float; o : float; 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) }; + inv_2 = position.Mctypes.y; + period_2 = Mctypes.t; + a_2_2 = inv_2; + o_3_2 = if (<=.)(0.000000, a_2_2) then a_2_2 else ~-.(a_2_2); + a_3 = l2_2; + o_2_2 = if (<=.)(0.000000, a_3) then a_3 else ~-.(a_3); + l2_2 = 0.000000 fby 0.000000 fby inv_2; + o_4 = + if (or)((<.)(o_2_2, 0.100000), (<.)(o_3_2, 0.100000)) + then 0.000000 + else 0.000000 -> (/.)((-.)(inv_2, l2_2), 2.000000 *. period_2); + inv = position.Mctypes.x; + period = Mctypes.t; + a_2_3 = inv; + o_3 = if (<=.)(0.000000, a_2_3) then a_2_3 else ~-.(a_2_3); + a_4 = l2; + o_2 = if (<=.)(0.000000, a_4) then a_4 else ~-.(a_4); + l2 = 0.000000 fby 0.000000 fby inv; + o = + if (or)((<.)(o_2, 0.100000), (<.)(o_3, 0.100000)) + then 0.000000 + else 0.000000 -> (/.)((-.)(inv, l2), 2.000000 *. period); + speed = { Mctypes.sx = o; Mctypes.sy = o_4 }; a_2 = x; b_2 = y; c_2 = Mathext.sqrtr((+.)(a_2 *. a_2, b_2 *. b_2)); @@ -645,7 +862,7 @@ let xnorm = (/.)(x, d); vr = ~-.((+.)(vx *. xnorm, vy *. ynorm)) end; - (x, y) = extracttrackposxy(track); + (x, y) = (x_2, y_2); rdrtrack = { Mctypes.r_pos = { Mctypes.x = x; Mctypes.y = y }; @@ -657,11 +874,11 @@ let v; Mctypes.r_sr = vr }; - v = vectnorme(vx, vy); - d = vectnorme(x, y); + v = c; + d = c_2; vy = l142.Mctypes.sy; vx = l142.Mctypes.sx; - l142 = calculatetrackspeedfrompos({ Mctypes.x = x; Mctypes.y = y }) + l142 = speed tel node risingEdge(re_Input : bool) returns (re_Output : bool) @@ -690,9 +907,9 @@ node mc_rdrstatecmd(rdronoffbutton : bool; currentrdrstate : Mctypes.tsensorstate) returns (rdronoffcmd : bool) var onoffbuttonpressed : bool; currentstate : Mctypes.tsensorstate; - onoffcmd : bool; + onoffcmd : bool; re_Input : bool; re_Output : bool; let - onoffbuttonpressed = risingEdge(rdronoffbutton); + onoffbuttonpressed = re_Output; currentstate = currentrdrstate; automaton state Off @@ -706,16 +923,18 @@ let unless | (&)(onoffbuttonpressed, (=)(currentstate, Mctypes.TState_ON)) then Off end; - rdronoffcmd = statecmd(risingEdge(rdronoffbutton), currentrdrstate) + re_Input = rdronoffbutton; + re_Output = (&)(not(re_Input -> pre re_Input), re_Input); + rdronoffcmd = onoffcmd tel node mc_iffstatecmd(iffonoffbutton : bool; currentiffstate : Mctypes.tsensorstate) returns (iffonoffcmd : bool) var onoffbuttonpressed : bool; currentstate : Mctypes.tsensorstate; - onoffcmd : bool; + onoffcmd : bool; re_Input : bool; re_Output : bool; let - onoffbuttonpressed = risingEdge(iffonoffbutton); + onoffbuttonpressed = re_Output; currentstate = currentiffstate; automaton state Off @@ -729,7 +948,9 @@ let unless | (&)(onoffbuttonpressed, (=)(currentstate, Mctypes.TState_ON)) then Off end; - iffonoffcmd = statecmd(risingEdge(iffonoffbutton), currentiffstate) + re_Input = iffonoffbutton; + re_Output = (&)(not(re_Input -> pre re_Input), re_Input); + iffonoffcmd = onoffcmd tel node rdrmodecmd(currentstate : Mctypes.tsensorstate; @@ -764,10 +985,11 @@ 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; + currentmode : Mctypes.trdrmode; modecmd : bool; re_Input : bool; + re_Output : bool; let currentstate = currentrdrstate; - modebuttonpressed = risingEdge(rdrmodebutton); + modebuttonpressed = re_Output; currentmode = currentrdrmode; automaton state Wide @@ -791,8 +1013,9 @@ let (=)(currentmode, Mctypes.TRdrMode_NARROW))) then Wide end; - rdrmodecmd = - rdrmodecmd(currentrdrstate, risingEdge(rdrmodebutton), currentrdrmode) + re_Input = rdrmodebutton; + re_Output = (&)(not(re_Input -> pre re_Input), re_Input); + rdrmodecmd = modecmd tel node radar_mode(modecmd : bool) returns (mode : Mctypes.trdrmode) @@ -867,9 +1090,9 @@ let 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) + rdrtracks = rdrtracks_2; + mode = mode_2; + (initializing, st) = (initializing_2, st_3) tel node iff_state(onoffcmd : bool; failure : bool) @@ -945,8 +1168,8 @@ let 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) + ifftracks = ifftracks_2; + (initializing, st) = (initializing_2, st_3) tel node advrandr(min : float; max : float) returns (output1 : float) @@ -968,42 +1191,80 @@ 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; +var min_5 : int; max_5 : int; step : int; l8 : int; output1_5 : int; + min_4 : float; max_4 : float; output1_4 : float; min_3 : float; + max_3 : float; output1_3 : float; min_2 : float; max_2 : float; + output1_2 : float; min : float; max : float; output1 : float; let - min = 0; - max = 1000; + min_5 = 0; + max_5 = 1000; step = 10; l8 = if not((=)(0, step)) then step else 1; - output1 = + output1_5 = (/) ((+) (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) + (Mc_ext.float_of_int((-)(max_5, min_5)) *. Mc_ext.rand()), min_5), + l8 * l8); + min_4 = 0.000000; + max_4 = 360.000000; + output1_4 = (+.)((-.)(max_4, min_4) *. Mc_ext.rand(), min_4); + min_3 = ~-.(10.000000); + max_3 = 10.000000; + output1_3 = (+.)((-.)(max_3, min_3) *. Mc_ext.rand(), min_3); + min_2 = ~-.(10.000000); + max_2 = 10.000000; + output1_2 = (+.)((-.)(max_2, min_2) *. Mc_ext.rand(), min_2); + min = 250.000000; + max = 1000.000000; + output1 = (+.)((-.)(max, min) *. Mc_ext.rand(), min); + speedinit = output1 *. Mctypes.t; + ymeterinit = Mctypes.nm *. output1_2; + xmeterinit = output1_3 *. Mctypes.nm; + sloperadinit = (/.)((2.000000 *. Mctypes.pi) *. output1_4, 360.000000); + idinit = output1_5 tel node createtracks_createonetrack_rand(res : bool) returns (track : Mctypes.ttrack) -var sloperadinit : float; speedinit : float; xmeterinit : float; +var min_5 : int; max_5 : int; step : int; l8 : int; output1_5 : int; + min_4 : float; max_4 : float; output1_4 : float; min_3 : float; + max_3 : float; output1_3 : float; min_2 : float; max_2 : float; + output1_2 : float; min : float; max : float; output1 : float; + 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); + min_5 = 0; + max_5 = 1000; + step = 10; + l8 = if not((=)(0, step)) then step else 1; + output1_5 = + (/) + ((+) + (Mc_ext.int_of_float + (Mc_ext.float_of_int((-)(max_5, min_5)) *. Mc_ext.rand()), min_5), + l8 * l8); + min_4 = 0.000000; + max_4 = 360.000000; + output1_4 = (+.)((-.)(max_4, min_4) *. Mc_ext.rand(), min_4); + min_3 = ~-.(10.000000); + max_3 = 10.000000; + output1_3 = (+.)((-.)(max_3, min_3) *. Mc_ext.rand(), min_3); + min_2 = ~-.(10.000000); + max_2 = 10.000000; + output1_2 = (+.)((-.)(max_2, min_2) *. Mc_ext.rand(), min_2); + min = 250.000000; + max = 1000.000000; + output1 = (+.)((-.)(max, min) *. Mc_ext.rand(), min); + speedinit = output1 *. Mctypes.t; + ymeterinit = Mctypes.nm *. output1_2; + xmeterinit = output1_3 *. Mctypes.nm; + sloperadinit = (/.)((2.000000 *. Mctypes.pi) *. output1_4, 360.000000); + idinit = output1_5; (sloperad, speedt, x0, y0, id) = if res - then createtracks_createonetrack_init_rand() + then (sloperadinit, speedinit, xmeterinit, ymeterinit, idinit) else (0.000000, 0.000000, 0.000000, 0.000000, 0) fby (sloperad, speedt, x0, y0, id) ; @@ -1025,7 +1286,14 @@ tel node createalltracks(res : bool) returns (tracks : Mctypes.ttracksarray) let - reset tracks = createtracks_rand(res) + reset + var res_2 : bool; tracks_2 : Mctypes.ttracksarray; in + + res_2 = res; + tracks_2 = + map<> createtracks_createonetrack_rand + <()>(res_2^Mctypes.ksizetracksarray); + tracks = tracks_2 every res tel @@ -1034,13 +1302,31 @@ node fusionrdrifftracks(iffmissiontrack : 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; + v2 : Mctypes.tspeed; speed1 : Mctypes.tspeed; speed2 : Mctypes.tspeed; + a_2_2 : float; o_2_2 : float; a_3 : float; o_3 : float; equal_3 : bool; + pos1_2 : Mctypes.tposition; pos2_2 : Mctypes.tposition; a_2 : float; + o_2 : float; a : float; o : float; equal_2 : bool; 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)); + speed1 = v1; + speed2 = v2; + a_2_2 = (-.)(speed1.Mctypes.sy, speed2.Mctypes.sy); + o_2_2 = if (<=.)(0.000000, a_2_2) then a_2_2 else ~-.(a_2_2); + a_3 = (-.)(speed1.Mctypes.sx, speed2.Mctypes.sx); + o_3 = if (<=.)(0.000000, a_3) then a_3 else ~-.(a_3); + equal_3 = (&)((<.)(o_3, 1.000000), (<.)(o_2_2, 1.000000)); + pos1_2 = pos1; + pos2_2 = pos2; + a_2 = (-.)(pos1_2.Mctypes.y, pos2_2.Mctypes.y); + o_2 = if (<=.)(0.000000, a_2) then a_2 else ~-.(a_2); + a = (-.)(pos1_2.Mctypes.x, pos2_2.Mctypes.x); + o = if (<=.)(0.000000, a) then a else ~-.(a); + equal_2 = (&)((<.)(o, 0.100000), (<.)(o_2, 0.100000)); + equal = (&)(equal_2, equal_3); newrdrmissiontrack = if l90 then { Mctypes.m_pos = @@ -1070,10 +1356,7 @@ let 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); + l90 = equal; newiffmissiontrack = if l90 then Mctypes.kinitmissiontrack else iffmissiontrack tel @@ -1119,11 +1402,34 @@ node prio_selecthighestprioritynotinpriorityarray(missiontrack : Mctypes.tmissio prioritiesarray : Mctypes.tpriorityList; accprioritymissiontrack : Mctypes.tmissiontrack) returns (prioritymissiontrack : Mctypes.tmissiontrack) -var missiontracknotinpriorittiesarray : bool; +var a : Mctypes.tmissiontrack; b : Mctypes.tmissiontrack; vr_2 : float; + d_2 : float; l13_2 : float; l11_2 : bool; result_2 : float; vr : float; + d : float; l13 : float; l11 : bool; result : float; prioritary : bool; + missiontracknotinpriorittiesarray : bool; missiontrackhashigherprioritythanacc : bool; let - missiontrackhashigherprioritythanacc = - not(trackalowerprioritythanb(missiontrack, accprioritymissiontrack)); + a = missiontrack; + b = accprioritymissiontrack; + vr_2 = b.Mctypes.m_sr; + d_2 = b.Mctypes.m_d; + result_2 = if l11_2 then l13_2 else 0.000000; + l13_2 = if l11_2 then (/.)(vr_2, d_2) else 0.000000 -> pre l13_2; + l11_2 = (>.)(d_2, 0.100000); + vr = a.Mctypes.m_sr; + d = a.Mctypes.m_d; + result = if l11 then l13 else 0.000000; + l13 = if l11 then (/.)(vr, d) else 0.000000 -> pre l13; + l11 = (>.)(d, 0.100000); + prioritary = + (or) + ((or) + ((=)(a.Mctypes.m_targettype, Mctypes.Ttargettype_friend), + not(a.Mctypes.m_detectedbyradar)), + (&) + ((&)(a.Mctypes.m_detectedbyradar, (<.)(result, result_2)), + b.Mctypes.m_detectedbyradar)) + ; + missiontrackhashigherprioritythanacc = not(prioritary); missiontracknotinpriorittiesarray = fold<<4>> prio_tracknumbernotinarray <()>(missiontrack.Mctypes.m_tracknumber^4, prioritiesarray, true); @@ -1164,7 +1470,7 @@ let if missiontrack_2.Mctypes.m_detectedbyradar then priority else 0}; missiontrackwithprio = if (=)(prioritytracknumber, missiontrack.Mctypes.m_tracknumber) - then setmissiontrackpriority(missiontrack, (+)(priorityindex, 1)) + then newmissiontrack else missiontrack tel @@ -1179,21 +1485,60 @@ tel node mc_tracks_prio(missiontracks : Mctypes.tmissiontracksarray) returns (missiontrackswithprio : Mctypes.tmissiontracksarray) -var missiontracks_2 : Mctypes.tmissiontracksarray; +var missiontracks_5 : Mctypes.tmissiontracksarray; + prioritiesarray_4 : Mctypes.tpriorityList; indexpriority_4 : int; + missiontrackwithhighestpriority_4 : Mctypes.tmissiontrack; + newprioritiesarray_4 : Mctypes.tpriorityList; + missiontracks_4 : Mctypes.tmissiontracksarray; + prioritiesarray_3 : Mctypes.tpriorityList; indexpriority_3 : int; + missiontrackwithhighestpriority_3 : Mctypes.tmissiontrack; + newprioritiesarray_3 : Mctypes.tpriorityList; + missiontracks_3 : Mctypes.tmissiontracksarray; + prioritiesarray_2 : Mctypes.tpriorityList; indexpriority_2 : int; + missiontrackwithhighestpriority_2 : Mctypes.tmissiontrack; + newprioritiesarray_2 : Mctypes.tpriorityList; + missiontracks_2 : Mctypes.tmissiontracksarray; prioritiesarray : Mctypes.tpriorityList; indexpriority : int; missiontrackwithhighestpriority : Mctypes.tmissiontrack; newprioritiesarray : Mctypes.tpriorityList; prioritytracknumbers : Mctypes.tpriorityList; let + missiontracks_5 = missiontracks; + prioritiesarray_4 = newprioritiesarray_3; + indexpriority_4 = 3; + newprioritiesarray_4 = + [prioritiesarray_4 with [indexpriority_4] = + missiontrackwithhighestpriority_4.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority_4 = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_5, + prioritiesarray_4^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontracks_4 = missiontracks; + prioritiesarray_3 = newprioritiesarray_2; + indexpriority_3 = 2; + newprioritiesarray_3 = + [prioritiesarray_3 with [indexpriority_3] = + missiontrackwithhighestpriority_3.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority_3 = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_4, + prioritiesarray_3^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontracks_3 = missiontracks; + prioritiesarray_2 = newprioritiesarray; + indexpriority_2 = 1; + newprioritiesarray_2 = + [prioritiesarray_2 with [indexpriority_2] = + missiontrackwithhighestpriority_2.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority_2 = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_3, + prioritiesarray_2^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); missiontracks_2 = missiontracks; - prioritiesarray = - prio_selectprioritarymissiontracks - (missiontracks, - prio_selectprioritarymissiontracks - (missiontracks, - prio_selectprioritarymissiontracks(missiontracks, 0^4, 0), 1), - 2); - indexpriority = 3; + prioritiesarray = 0^4; + indexpriority = 0; newprioritiesarray = [prioritiesarray with [indexpriority] = missiontrackwithhighestpriority.Mctypes.m_tracknumber]; @@ -1204,16 +1549,7 @@ let 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) + prioritytracknumbers = newprioritiesarray_4 tel node mc_tracks_tracknumber(withouttracknb : Mctypes.tmissiontracksarray) @@ -1229,28 +1565,102 @@ tel node mc_tracks(rdrtracks : Mctypes.trdrtracksarray; ifftracks : Mctypes.tifftracksarray) returns (missiontracks : Mctypes.tmissiontracksarray) -var missiontracks_2 : Mctypes.tmissiontracksarray; +var missiontracks_6 : Mctypes.tmissiontracksarray; + missiontracks_5 : Mctypes.tmissiontracksarray; + prioritiesarray_4 : Mctypes.tpriorityList; indexpriority_4 : int; + missiontrackwithhighestpriority_4 : Mctypes.tmissiontrack; + newprioritiesarray_4 : Mctypes.tpriorityList; + missiontracks_4 : Mctypes.tmissiontracksarray; + prioritiesarray_3 : Mctypes.tpriorityList; indexpriority_3 : int; + missiontrackwithhighestpriority_3 : Mctypes.tmissiontrack; + newprioritiesarray_3 : Mctypes.tpriorityList; + missiontracks_3 : Mctypes.tmissiontracksarray; + prioritiesarray_2 : Mctypes.tpriorityList; indexpriority_2 : int; + missiontrackwithhighestpriority_2 : Mctypes.tmissiontrack; + newprioritiesarray_2 : Mctypes.tpriorityList; + missiontracks_2_2 : Mctypes.tmissiontracksarray; + prioritiesarray : Mctypes.tpriorityList; indexpriority : int; + missiontrackwithhighestpriority : Mctypes.tmissiontrack; + newprioritiesarray : Mctypes.tpriorityList; prioritytracknumbers : Mctypes.tpriorityList; missiontrackswithprio : Mctypes.tmissiontracksarray; + withouttracknb : Mctypes.tmissiontracksarray; l81 : int; + withtracknumber : Mctypes.tmissiontracksarray; + rdrtracks_2 : Mctypes.trdrtracksarray; + ifftracks_2 : Mctypes.tifftracksarray; + mergedrdrtracks : Mctypes.tmissiontrack^Mctypes.ksizerdrtracksarray; + mergedifftracks : Mctypes.tmissiontrack^Mctypes.ksizeifftracksarray; + l140 : Mctypes.tmissiontrack^Mctypes.ksizerdrtracksarray; + l139 : Mctypes.tmissiontrack^Mctypes.ksizeifftracksarray; + missiontracks_2 : Mctypes.tmissiontracksarray; let - missiontracks_2 = - mc_tracks_tracknumber(mc_tracks_fusion(rdrtracks, ifftracks)); + missiontracks_6 = withtracknumber; + missiontracks_5 = missiontracks_6; + prioritiesarray_4 = newprioritiesarray_3; + indexpriority_4 = 3; + newprioritiesarray_4 = + [prioritiesarray_4 with [indexpriority_4] = + missiontrackwithhighestpriority_4.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority_4 = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_5, + prioritiesarray_4^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontracks_4 = missiontracks_6; + prioritiesarray_3 = newprioritiesarray_2; + indexpriority_3 = 2; + newprioritiesarray_3 = + [prioritiesarray_3 with [indexpriority_3] = + missiontrackwithhighestpriority_3.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority_3 = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_4, + prioritiesarray_3^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontracks_3 = missiontracks_6; + prioritiesarray_2 = newprioritiesarray; + indexpriority_2 = 1; + newprioritiesarray_2 = + [prioritiesarray_2 with [indexpriority_2] = + missiontrackwithhighestpriority_2.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority_2 = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_3, + prioritiesarray_2^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontracks_2_2 = missiontracks_6; + prioritiesarray = 0^4; + indexpriority = 0; + newprioritiesarray = + [prioritiesarray with [indexpriority] = + missiontrackwithhighestpriority.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_2_2, + prioritiesarray^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); 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))) + <(prioritytracknumbers)>(missiontracks_6); + prioritytracknumbers = newprioritiesarray_4; + withouttracknb = missiontracks_2; + (withtracknumber, l81) = + mapfold<> calculatemissiontracknumber + <(Mctypes.kinitmissiontrackarray -> pre withtracknumber)>(withouttracknb, + 0 -> pre l81); + rdrtracks_2 = rdrtracks; + ifftracks_2 = ifftracks; + missiontracks_2 = mergedrdrtracks @ mergedifftracks; + (mergedrdrtracks, mergedifftracks) = + mapfold<> mc_tracks_fusion_onerdrwithifftracks + <()>(l140, l139); + l140 = + map<> convertrdrtracktomissiontrack + <()>(rdrtracks_2); + l139 = + map<> convertifftracktomissiontrack + <()>(ifftracks_2); + missiontracks = missiontrackswithprio tel node mc(currentrdrstate : Mctypes.tsensorstate; @@ -1262,35 +1672,190 @@ node mc(currentrdrstate : Mctypes.tsensorstate; returns (rdronoffcmd : bool; rdrmodecmd : bool; missiontracks : Mctypes.tmissiontracksarray; iffonoffcmd : bool) var rdronoffbutton_2 : bool; currentrdrstate_3 : Mctypes.tsensorstate; + onoffbuttonpressed_2 : bool; currentstate_3 : Mctypes.tsensorstate; + onoffcmd_2 : bool; re_Input_3 : bool; re_Output_3 : bool; 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; + currentstate_2 : Mctypes.tsensorstate; modebuttonpressed : bool; + currentmode : Mctypes.trdrmode; modecmd : bool; re_Input_2 : bool; + re_Output_2 : bool; rdrmodecmd_2 : bool; iffonoffbutton_2 : bool; + currentiffstate_2 : Mctypes.tsensorstate; onoffbuttonpressed : bool; + currentstate : Mctypes.tsensorstate; onoffcmd : bool; re_Input : bool; + re_Output : bool; iffonoffcmd_2 : bool; + rdrtracks_3 : Mctypes.trdrtracksarray; + ifftracks_3 : Mctypes.tifftracksarray; + missiontracks_6 : Mctypes.tmissiontracksarray; + missiontracks_5 : Mctypes.tmissiontracksarray; + prioritiesarray_4 : Mctypes.tpriorityList; indexpriority_4 : int; + missiontrackwithhighestpriority_4 : Mctypes.tmissiontrack; + newprioritiesarray_4 : Mctypes.tpriorityList; + missiontracks_4 : Mctypes.tmissiontracksarray; + prioritiesarray_3 : Mctypes.tpriorityList; indexpriority_3 : int; + missiontrackwithhighestpriority_3 : Mctypes.tmissiontrack; + newprioritiesarray_3 : Mctypes.tpriorityList; + missiontracks_3 : Mctypes.tmissiontracksarray; + prioritiesarray_2 : Mctypes.tpriorityList; indexpriority_2 : int; + missiontrackwithhighestpriority_2 : Mctypes.tmissiontrack; + newprioritiesarray_2 : Mctypes.tpriorityList; + missiontracks_2_2 : Mctypes.tmissiontracksarray; + prioritiesarray : Mctypes.tpriorityList; indexpriority : int; + missiontrackwithhighestpriority : Mctypes.tmissiontrack; + newprioritiesarray : Mctypes.tpriorityList; + prioritytracknumbers : Mctypes.tpriorityList; + missiontrackswithprio : Mctypes.tmissiontracksarray; + withouttracknb : Mctypes.tmissiontracksarray; l81 : int; + withtracknumber : Mctypes.tmissiontracksarray; rdrtracks_2 : Mctypes.trdrtracksarray; ifftracks_2 : Mctypes.tifftracksarray; + mergedrdrtracks : Mctypes.tmissiontrack^Mctypes.ksizerdrtracksarray; + mergedifftracks : Mctypes.tmissiontrack^Mctypes.ksizeifftracksarray; + l140 : Mctypes.tmissiontrack^Mctypes.ksizerdrtracksarray; + l139 : Mctypes.tmissiontrack^Mctypes.ksizeifftracksarray; missiontracks_2 : Mctypes.tmissiontracksarray; + missiontracks_7 : Mctypes.tmissiontracksarray; let rdronoffbutton_2 = rdronoffbutton; currentrdrstate_3 = currentrdrstate; - rdronoffcmd_2 = statecmd(risingEdge(rdronoffbutton_2), currentrdrstate_3); + onoffbuttonpressed_2 = re_Output_3; + currentstate_3 = currentrdrstate_3; + automaton + state Off + do + onoffcmd_2 = false + unless + | (&)(onoffbuttonpressed_2, (=)(currentstate_3, Mctypes.TState_OFF)) then On + state On + do + onoffcmd_2 = true + unless + | (&)(onoffbuttonpressed_2, (=)(currentstate_3, Mctypes.TState_ON)) then Off + end; + re_Input_3 = rdronoffbutton_2; + re_Output_3 = (&)(not(re_Input_3 -> pre re_Input_3), re_Input_3); + rdronoffcmd_2 = onoffcmd_2; currentrdrstate_2 = currentrdrstate; rdrmodebutton_2 = rdrmodebutton; currentrdrmode_2 = currentrdrmode; - rdrmodecmd_2 = - rdrmodecmd - (currentrdrstate_2, risingEdge(rdrmodebutton_2), currentrdrmode_2); + currentstate_2 = currentrdrstate_2; + modebuttonpressed = re_Output_2; + currentmode = currentrdrmode_2; + automaton + state Wide + do + modecmd = false + unless + | (&) + (modebuttonpressed, + (&) + ((=)(currentstate_2, Mctypes.TState_ON), + (=)(currentmode, Mctypes.TRdrMode_WIDE))) + then Narrow + state Narrow + do + modecmd = true + unless + | (&) + (modebuttonpressed, + (&) + ((=)(currentstate_2, Mctypes.TState_ON), + (=)(currentmode, Mctypes.TRdrMode_NARROW))) + then Wide + end; + re_Input_2 = rdrmodebutton_2; + re_Output_2 = (&)(not(re_Input_2 -> pre re_Input_2), re_Input_2); + rdrmodecmd_2 = modecmd; 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) + onoffbuttonpressed = re_Output; + currentstate = currentiffstate_2; + 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; + re_Input = iffonoffbutton_2; + re_Output = (&)(not(re_Input -> pre re_Input), re_Input); + iffonoffcmd_2 = onoffcmd; + rdrtracks_3 = rdrtracks; + ifftracks_3 = ifftracks; + missiontracks_6 = withtracknumber; + missiontracks_5 = missiontracks_6; + prioritiesarray_4 = newprioritiesarray_3; + indexpriority_4 = 3; + newprioritiesarray_4 = + [prioritiesarray_4 with [indexpriority_4] = + missiontrackwithhighestpriority_4.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority_4 = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_5, + prioritiesarray_4^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontracks_4 = missiontracks_6; + prioritiesarray_3 = newprioritiesarray_2; + indexpriority_3 = 2; + newprioritiesarray_3 = + [prioritiesarray_3 with [indexpriority_3] = + missiontrackwithhighestpriority_3.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority_3 = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_4, + prioritiesarray_3^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontracks_3 = missiontracks_6; + prioritiesarray_2 = newprioritiesarray; + indexpriority_2 = 1; + newprioritiesarray_2 = + [prioritiesarray_2 with [indexpriority_2] = + missiontrackwithhighestpriority_2.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority_2 = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_3, + prioritiesarray_2^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontracks_2_2 = missiontracks_6; + prioritiesarray = 0^4; + indexpriority = 0; + newprioritiesarray = + [prioritiesarray with [indexpriority] = + missiontrackwithhighestpriority.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_2_2, + prioritiesarray^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontrackswithprio = + map<> prio_setpriorityinmissiontrackarray + <(prioritytracknumbers)>(missiontracks_6); + prioritytracknumbers = newprioritiesarray_4; + withouttracknb = missiontracks_2; + (withtracknumber, l81) = + mapfold<> calculatemissiontracknumber + <(Mctypes.kinitmissiontrackarray -> pre withtracknumber)>(withouttracknb, + 0 -> pre l81); + rdrtracks_2 = rdrtracks_3; + ifftracks_2 = ifftracks_3; + missiontracks_2 = mergedrdrtracks @ mergedifftracks; + (mergedrdrtracks, mergedifftracks) = + mapfold<> mc_tracks_fusion_onerdrwithifftracks + <()>(l140, l139); + l140 = + map<> convertrdrtracktomissiontrack + <()>(rdrtracks_2); + l139 = + map<> convertifftracktomissiontrack + <()>(ifftracks_2); + missiontracks_7 = missiontrackswithprio; + missiontracks = missiontracks_7; + iffonoffcmd = iffonoffcmd_2; + rdrmodecmd = rdrmodecmd_2; + rdronoffcmd = rdronoffcmd_2 tel node implies(a : bool; b : bool) returns (c : bool) @@ -1335,18 +1900,14 @@ tel node dv_proof1(currentrdrstate : Mctypes.tsensorstate; rdronoffbutton : bool; rdronoffcmd : bool) returns (proof1 : bool) -var a : bool; b : bool; c : bool; +var a : bool; b : bool; c : bool; re_Input : bool; re_Output : bool; let - a = - (&) - (risingEdge(rdronoffbutton), (=)(currentrdrstate, Mctypes.TState_FAIL)); + a = (&)(re_Output, (=)(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)) + re_Input = rdronoffbutton; + re_Output = (&)(not(re_Input -> pre re_Input), re_Input); + proof1 = c tel node dv_proof2(ifftracks : Mctypes.tifftracksarray; @@ -1360,7 +1921,7 @@ let l33 = fold<> dv_detectedbyiff <()>(missiontracks, true); - proof2 = implies((=)(ifftracks, Mctypes.kinitifftrackarray), l33) + proof2 = c tel node dv_proof3(missiontracks : Mctypes.tmissiontracksarray) @@ -1381,100 +1942,381 @@ node dv_observer(currentrdrstate : Mctypes.tsensorstate; currentiffstate : Mctypes.tsensorstate; ifftracks : Mctypes.tifftracksarray) returns (proof1 : bool; proof2 : bool; proof3 : bool) -var currentrdrstate_3 : Mctypes.tsensorstate; +var currentrdrstate_4 : Mctypes.tsensorstate; + currentrdrmode_3 : Mctypes.trdrmode; + rdrtracks_4 : Mctypes.trdrtracksarray; rdronoffbutton_3 : bool; + rdrmodebutton_3 : bool; iffonoffbutton_3 : bool; + currentiffstate_3 : Mctypes.tsensorstate; + ifftracks_4 : Mctypes.tifftracksarray; rdronoffbutton_2_2 : bool; + currentrdrstate_3 : Mctypes.tsensorstate; onoffbuttonpressed_2 : bool; + currentstate_3 : Mctypes.tsensorstate; onoffcmd_2 : bool; + re_Input_3 : bool; re_Output_3 : bool; rdronoffcmd_2 : bool; + currentrdrstate_2_2 : Mctypes.tsensorstate; rdrmodebutton_2 : bool; 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; + currentstate_2 : Mctypes.tsensorstate; modebuttonpressed : bool; + currentmode : Mctypes.trdrmode; modecmd : bool; re_Input_2 : bool; + re_Output_2 : bool; rdrmodecmd_2 : bool; iffonoffbutton_2 : bool; + currentiffstate_2 : Mctypes.tsensorstate; onoffbuttonpressed : bool; + currentstate : Mctypes.tsensorstate; onoffcmd : bool; re_Input_4 : bool; + re_Output_4 : bool; iffonoffcmd_2 : bool; + rdrtracks_3 : Mctypes.trdrtracksarray; + ifftracks_3 : Mctypes.tifftracksarray; + missiontracks_6 : Mctypes.tmissiontracksarray; + missiontracks_5 : Mctypes.tmissiontracksarray; + prioritiesarray_4 : Mctypes.tpriorityList; indexpriority_4 : int; + missiontrackwithhighestpriority_4 : Mctypes.tmissiontrack; + newprioritiesarray_4 : Mctypes.tpriorityList; + missiontracks_4 : Mctypes.tmissiontracksarray; + prioritiesarray_3 : Mctypes.tpriorityList; indexpriority_3 : int; + missiontrackwithhighestpriority_3 : Mctypes.tmissiontrack; + newprioritiesarray_3 : Mctypes.tpriorityList; + missiontracks_3 : Mctypes.tmissiontracksarray; + prioritiesarray_2 : Mctypes.tpriorityList; indexpriority_2 : int; + missiontrackwithhighestpriority_2 : Mctypes.tmissiontrack; + newprioritiesarray_2 : Mctypes.tpriorityList; + missiontracks_2_2 : Mctypes.tmissiontracksarray; + prioritiesarray : Mctypes.tpriorityList; indexpriority : int; + missiontrackwithhighestpriority : Mctypes.tmissiontrack; + newprioritiesarray : Mctypes.tpriorityList; + prioritytracknumbers : Mctypes.tpriorityList; + missiontrackswithprio : Mctypes.tmissiontracksarray; + withouttracknb : Mctypes.tmissiontracksarray; l81 : int; + withtracknumber : Mctypes.tmissiontracksarray; + rdrtracks_2 : Mctypes.trdrtracksarray; + ifftracks_2_2 : Mctypes.tifftracksarray; + mergedrdrtracks : Mctypes.tmissiontrack^Mctypes.ksizerdrtracksarray; + mergedifftracks : Mctypes.tmissiontrack^Mctypes.ksizeifftracksarray; + l140 : Mctypes.tmissiontrack^Mctypes.ksizerdrtracksarray; + l139 : Mctypes.tmissiontrack^Mctypes.ksizeifftracksarray; + missiontracks_2_3 : Mctypes.tmissiontracksarray; + missiontracks_7 : Mctypes.tmissiontracksarray; rdronoffcmd_3 : bool; + rdrmodecmd : bool; missiontracks_8 : Mctypes.tmissiontracksarray; iffonoffcmd : bool; currentrdrstate_2 : Mctypes.tsensorstate; - rdronoffbutton_2 : bool; rdronoffcmd : bool; proof1_2 : bool; + rdronoffbutton_2 : bool; rdronoffcmd : bool; a_2 : bool; b_2 : bool; + c_2 : bool; re_Input : bool; re_Output : 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; + missiontracks_2 : Mctypes.tmissiontracksarray; a : bool; b : bool; + c : bool; 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; + currentrdrstate_4 = currentrdrstate; + currentrdrmode_3 = currentrdrmode; + rdrtracks_4 = 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); + rdrmodebutton_3 = rdrmodebutton; + iffonoffbutton_3 = iffonoffbutton; + currentiffstate_3 = currentiffstate; + ifftracks_4 = ifftracks; + rdronoffbutton_2_2 = rdronoffbutton_3; + currentrdrstate_3 = currentrdrstate_4; + onoffbuttonpressed_2 = re_Output_3; + currentstate_3 = currentrdrstate_3; + automaton + state Off + do + onoffcmd_2 = false + unless + | (&)(onoffbuttonpressed_2, (=)(currentstate_3, Mctypes.TState_OFF)) then On + state On + do + onoffcmd_2 = true + unless + | (&)(onoffbuttonpressed_2, (=)(currentstate_3, Mctypes.TState_ON)) then Off + end; + re_Input_3 = rdronoffbutton_2_2; + re_Output_3 = (&)(not(re_Input_3 -> pre re_Input_3), re_Input_3); + rdronoffcmd_2 = onoffcmd_2; + currentrdrstate_2_2 = currentrdrstate_4; + rdrmodebutton_2 = rdrmodebutton_3; + currentrdrmode_2 = currentrdrmode_3; + currentstate_2 = currentrdrstate_2_2; + modebuttonpressed = re_Output_2; + currentmode = currentrdrmode_2; + automaton + state Wide + do + modecmd = false + unless + | (&) + (modebuttonpressed, + (&) + ((=)(currentstate_2, Mctypes.TState_ON), + (=)(currentmode, Mctypes.TRdrMode_WIDE))) + then Narrow + state Narrow + do + modecmd = true + unless + | (&) + (modebuttonpressed, + (&) + ((=)(currentstate_2, Mctypes.TState_ON), + (=)(currentmode, Mctypes.TRdrMode_NARROW))) + then Wide + end; + re_Input_2 = rdrmodebutton_2; + re_Output_2 = (&)(not(re_Input_2 -> pre re_Input_2), re_Input_2); + rdrmodecmd_2 = modecmd; + iffonoffbutton_2 = iffonoffbutton_3; + currentiffstate_2 = currentiffstate_3; + onoffbuttonpressed = re_Output_4; + currentstate = currentiffstate_2; + 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; + re_Input_4 = iffonoffbutton_2; + re_Output_4 = (&)(not(re_Input_4 -> pre re_Input_4), re_Input_4); + iffonoffcmd_2 = onoffcmd; + rdrtracks_3 = rdrtracks_4; + ifftracks_3 = ifftracks_4; + missiontracks_6 = withtracknumber; + missiontracks_5 = missiontracks_6; + prioritiesarray_4 = newprioritiesarray_3; + indexpriority_4 = 3; + newprioritiesarray_4 = + [prioritiesarray_4 with [indexpriority_4] = + missiontrackwithhighestpriority_4.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority_4 = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_5, + prioritiesarray_4^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontracks_4 = missiontracks_6; + prioritiesarray_3 = newprioritiesarray_2; + indexpriority_3 = 2; + newprioritiesarray_3 = + [prioritiesarray_3 with [indexpriority_3] = + missiontrackwithhighestpriority_3.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority_3 = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_4, + prioritiesarray_3^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontracks_3 = missiontracks_6; + prioritiesarray_2 = newprioritiesarray; + indexpriority_2 = 1; + newprioritiesarray_2 = + [prioritiesarray_2 with [indexpriority_2] = + missiontrackwithhighestpriority_2.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority_2 = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_3, + prioritiesarray_2^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontracks_2_2 = missiontracks_6; + prioritiesarray = 0^4; + indexpriority = 0; + newprioritiesarray = + [prioritiesarray with [indexpriority] = + missiontrackwithhighestpriority.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_2_2, + prioritiesarray^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontrackswithprio = + map<> prio_setpriorityinmissiontrackarray + <(prioritytracknumbers)>(missiontracks_6); + prioritytracknumbers = newprioritiesarray_4; + withouttracknb = missiontracks_2_3; + (withtracknumber, l81) = + mapfold<> calculatemissiontracknumber + <(Mctypes.kinitmissiontrackarray -> pre withtracknumber)>(withouttracknb, + 0 -> pre l81); + rdrtracks_2 = rdrtracks_3; + ifftracks_2_2 = ifftracks_3; + missiontracks_2_3 = mergedrdrtracks @ mergedifftracks; + (mergedrdrtracks, mergedifftracks) = + mapfold<> mc_tracks_fusion_onerdrwithifftracks + <()>(l140, l139); + l140 = + map<> convertrdrtracktomissiontrack + <()>(rdrtracks_2); + l139 = + map<> convertifftracktomissiontrack + <()>(ifftracks_2_2); + missiontracks_7 = missiontrackswithprio; + missiontracks_8 = missiontracks_7; + iffonoffcmd = iffonoffcmd_2; + rdrmodecmd = rdrmodecmd_2; + rdronoffcmd_3 = rdronoffcmd_2; currentrdrstate_2 = currentrdrstate; rdronoffbutton_2 = rdronoffbutton; rdronoffcmd = l1; - proof1_2 = - implies - ((&) - (risingEdge(rdronoffbutton_2), - (=)(currentrdrstate_2, Mctypes.TState_FAIL)), - (=)(rdronoffcmd, false -> pre rdronoffcmd)); + a_2 = (&)(re_Output, (=)(currentrdrstate_2, Mctypes.TState_FAIL)); + b_2 = (=)(rdronoffcmd, false -> pre rdronoffcmd); + c_2 = (or)(not(a_2), b_2); + re_Input = rdronoffbutton_2; + re_Output = (&)(not(re_Input -> pre re_Input), re_Input); + proof1_2 = c_2; ifftracks_2 = ifftracks; missiontracks_2 = l3; + a = (=)(ifftracks_2, Mctypes.kinitifftrackarray); + b = l33_2; + c = (or)(not(a), b); l33_2 = fold<> dv_detectedbyiff <()>(missiontracks_2, true); - proof2_2 = implies((=)(ifftracks_2, Mctypes.kinitifftrackarray), l33_2); + proof2_2 = c; 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); + proof3 = proof3_2; + proof2 = proof2_2; + proof1 = proof1_2; (l1, l4, l3, l5) = - mc - (currentrdrstate, currentrdrmode, rdrtracks, rdronoffbutton, - rdrmodebutton, iffonoffbutton, currentiffstate, ifftracks) + (rdronoffcmd_3, rdrmodecmd, missiontracks_8, iffonoffcmd) tel node fighterdebug(res : bool; rdronoffclicked : bool; iffonoffclicked : bool) returns (missiontracks : Mctypes.tmissiontracksarray) -var onoffcmd_2 : bool; modecmd : bool; failure_2 : bool; +var onoffcmd_4 : bool; modecmd_3 : bool; failure_3 : 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; + tracks_4 : Mctypes.ttracksarray; onoffcmd_2_3 : bool; failure_2_2 : bool; + x_2 : bool; initializing_2_2 : bool; st_3_2 : Mctypes.tsensorstate; + modecmd_2 : bool; mode_2 : Mctypes.trdrmode; + st_2_2 : Mctypes.tsensorstate; tracks_2_2 : Mctypes.ttracksarray; + rdrdetectedtracks_2 : Mctypes.tdetectedrdrtracksarray; + l22 : Mctypes.ttrack^Mctypes.ksizerdrtracksarray; + l30 : Mctypes.trdrtrack^Mctypes.ksizerdrtracksarray; + rdrtracks_2_2 : Mctypes.trdrtracksarray; initializing_3 : bool; + st_4 : Mctypes.tsensorstate; mode : Mctypes.trdrmode; + rdrtracks_4 : Mctypes.trdrtracksarray; tracks_3 : Mctypes.ttracksarray; failure : bool; iffdetectedtracks : Mctypes.tdetectedifftracksarray; - onoffcmd : bool; st : Mctypes.tsensorstate; - ifftracks_2 : Mctypes.tifftracksarray; initializing : bool; - currentrdrstate : Mctypes.tsensorstate; + onoffcmd_3 : bool; onoffcmd_2_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_2 : Mctypes.tifftracksarray; + st : Mctypes.tsensorstate; ifftracks_4 : 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; + ifftracks : Mctypes.tifftracksarray; rdronoffbutton_2 : bool; + currentrdrstate_3 : Mctypes.tsensorstate; onoffbuttonpressed_2 : bool; + currentstate_3 : Mctypes.tsensorstate; onoffcmd_2 : bool; + re_Input_3 : bool; re_Output_3 : bool; rdronoffcmd_2 : bool; + currentrdrstate_2 : Mctypes.tsensorstate; rdrmodebutton_2 : bool; + currentrdrmode_2 : Mctypes.trdrmode; + currentstate_2 : Mctypes.tsensorstate; modebuttonpressed : bool; + currentmode : Mctypes.trdrmode; modecmd : bool; re_Input_2 : bool; + re_Output_2 : bool; rdrmodecmd_2 : bool; iffonoffbutton_2 : bool; + currentiffstate_2 : Mctypes.tsensorstate; onoffbuttonpressed : bool; + currentstate : Mctypes.tsensorstate; onoffcmd : bool; re_Input : bool; + re_Output : bool; iffonoffcmd_2 : bool; + rdrtracks_3 : Mctypes.trdrtracksarray; + ifftracks_3 : Mctypes.tifftracksarray; + missiontracks_6 : Mctypes.tmissiontracksarray; + missiontracks_5 : Mctypes.tmissiontracksarray; + prioritiesarray_4 : Mctypes.tpriorityList; indexpriority_4 : int; + missiontrackwithhighestpriority_4 : Mctypes.tmissiontrack; + newprioritiesarray_4 : Mctypes.tpriorityList; + missiontracks_4 : Mctypes.tmissiontracksarray; + prioritiesarray_3 : Mctypes.tpriorityList; indexpriority_3 : int; + missiontrackwithhighestpriority_3 : Mctypes.tmissiontrack; + newprioritiesarray_3 : Mctypes.tpriorityList; + missiontracks_3 : Mctypes.tmissiontracksarray; + prioritiesarray_2 : Mctypes.tpriorityList; indexpriority_2 : int; + missiontrackwithhighestpriority_2 : Mctypes.tmissiontrack; + newprioritiesarray_2 : Mctypes.tpriorityList; + missiontracks_2_2 : Mctypes.tmissiontracksarray; + prioritiesarray : Mctypes.tpriorityList; indexpriority : int; + missiontrackwithhighestpriority : Mctypes.tmissiontrack; + newprioritiesarray : Mctypes.tpriorityList; + prioritytracknumbers : Mctypes.tpriorityList; + missiontrackswithprio : Mctypes.tmissiontracksarray; + withouttracknb : Mctypes.tmissiontracksarray; l81 : int; + withtracknumber : Mctypes.tmissiontracksarray; + rdrtracks_2 : Mctypes.trdrtracksarray; + ifftracks_2 : Mctypes.tifftracksarray; + mergedrdrtracks : Mctypes.tmissiontrack^Mctypes.ksizerdrtracksarray; + mergedifftracks : Mctypes.tmissiontrack^Mctypes.ksizeifftracksarray; + l140 : Mctypes.tmissiontrack^Mctypes.ksizerdrtracksarray; + l139 : Mctypes.tmissiontrack^Mctypes.ksizeifftracksarray; + missiontracks_2 : Mctypes.tmissiontracksarray; + missiontracks_7 : Mctypes.tmissiontracksarray; rdronoffcmd : bool; + rdrmodecmd : bool; missiontracks_8 : Mctypes.tmissiontracksarray; + iffonoffcmd : bool; 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; + onoffcmd_4 = false -> pre l10; + modecmd_3 = false -> pre l11; + failure_3 = false; rdrdetectedtracks = [0, 1, 2, 3, 4]; + tracks_4 = l179; + onoffcmd_2_3 = onoffcmd_4; + failure_2_2 = failure_3; + initializing_2_2 = (&)((=)(st_3_2, Mctypes.TState_OFF), onoffcmd_2_3); + x_2 = false fby false fby false fby false fby false fby onoffcmd_2_3; + st_3_2 = + if failure_2_2 + then Mctypes.TState_FAIL + else if if onoffcmd_2_3 then x_2 else false + then Mctypes.TState_ON + else Mctypes.TState_OFF + ; + modecmd_2 = modecmd_3; + mode_2 = + if modecmd_2 then Mctypes.TRdrMode_NARROW else Mctypes.TRdrMode_WIDE; + st_2_2 = st_4; + tracks_2_2 = tracks_4; + rdrdetectedtracks_2 = rdrdetectedtracks; + rdrtracks_2_2 = + if (=)(st_2_2, Mctypes.TState_ON) + then l30 + else Mctypes.kinitrdrtrackarray; + l30 = map<> elaboraterdrtrack<()>(l22); + l22 = + map<> selectdetectedtrack + <()>(rdrdetectedtracks_2, tracks_2_2^Mctypes.ksizerdrtracksarray, + Mctypes.kinittrack^Mctypes.ksizerdrtracksarray); + rdrtracks_4 = rdrtracks_2_2; + mode = mode_2; + (initializing_3, st_4) = (initializing_2_2, st_3_2); 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); + onoffcmd_3 = false -> pre l12; + onoffcmd_2_2 = onoffcmd_3; + failure_2 = failure; + initializing_2 = (&)((=)(st_3, Mctypes.TState_OFF), onoffcmd_2_2); + x = false fby false fby false fby false fby false fby onoffcmd_2_2; + st_3 = + if failure_2 + then Mctypes.TState_FAIL + else if if onoffcmd_2_2 then x else false + then Mctypes.TState_ON + else Mctypes.TState_OFF + ; + st_2 = st; + tracks_2 = tracks_3; + iffdetectedtracks_2 = iffdetectedtracks; + l34 = + map<> selectdetectedtrack + <()>(iffdetectedtracks_2, tracks_2^Mctypes.ksizeifftracksarray, + Mctypes.kinittrack^Mctypes.ksizeifftracksarray); + l40 = map<> ifftrack_of_track<()>(l34); + ifftracks_2_2 = + if (=)(st_2, Mctypes.TState_ON) then l40 else Mctypes.kinitifftrackarray; + ifftracks_4 = ifftracks_2_2; + (initializing, st) = (initializing_2, st_3); currentrdrstate = l172; currentrdrmode = l3; rdrtracks = l4; @@ -1483,33 +2325,460 @@ let 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; + rdronoffbutton_2 = rdronoffbutton; + currentrdrstate_3 = currentrdrstate; + onoffbuttonpressed_2 = re_Output_3; + currentstate_3 = currentrdrstate_3; + automaton + state Off + do + onoffcmd_2 = false + unless + | (&)(onoffbuttonpressed_2, (=)(currentstate_3, Mctypes.TState_OFF)) then On + state On + do + onoffcmd_2 = true + unless + | (&)(onoffbuttonpressed_2, (=)(currentstate_3, Mctypes.TState_ON)) then Off + end; + re_Input_3 = rdronoffbutton_2; + re_Output_3 = (&)(not(re_Input_3 -> pre re_Input_3), re_Input_3); + rdronoffcmd_2 = onoffcmd_2; + currentrdrstate_2 = currentrdrstate; + rdrmodebutton_2 = rdrmodebutton; + currentrdrmode_2 = currentrdrmode; + currentstate_2 = currentrdrstate_2; + modebuttonpressed = re_Output_2; + currentmode = currentrdrmode_2; + automaton + state Wide + do + modecmd = false + unless + | (&) + (modebuttonpressed, + (&) + ((=)(currentstate_2, Mctypes.TState_ON), + (=)(currentmode, Mctypes.TRdrMode_WIDE))) + then Narrow + state Narrow + do + modecmd = true + unless + | (&) + (modebuttonpressed, + (&) + ((=)(currentstate_2, Mctypes.TState_ON), + (=)(currentmode, Mctypes.TRdrMode_NARROW))) + then Wide + end; + re_Input_2 = rdrmodebutton_2; + re_Output_2 = (&)(not(re_Input_2 -> pre re_Input_2), re_Input_2); + rdrmodecmd_2 = modecmd; + iffonoffbutton_2 = iffonoffbutton; + currentiffstate_2 = currentiffstate; + onoffbuttonpressed = re_Output; + currentstate = currentiffstate_2; + 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; + re_Input = iffonoffbutton_2; + re_Output = (&)(not(re_Input -> pre re_Input), re_Input); + iffonoffcmd_2 = onoffcmd; + rdrtracks_3 = rdrtracks; + ifftracks_3 = ifftracks; + missiontracks_6 = withtracknumber; + missiontracks_5 = missiontracks_6; + prioritiesarray_4 = newprioritiesarray_3; + indexpriority_4 = 3; + newprioritiesarray_4 = + [prioritiesarray_4 with [indexpriority_4] = + missiontrackwithhighestpriority_4.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority_4 = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_5, + prioritiesarray_4^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontracks_4 = missiontracks_6; + prioritiesarray_3 = newprioritiesarray_2; + indexpriority_3 = 2; + newprioritiesarray_3 = + [prioritiesarray_3 with [indexpriority_3] = + missiontrackwithhighestpriority_3.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority_3 = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_4, + prioritiesarray_3^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontracks_3 = missiontracks_6; + prioritiesarray_2 = newprioritiesarray; + indexpriority_2 = 1; + newprioritiesarray_2 = + [prioritiesarray_2 with [indexpriority_2] = + missiontrackwithhighestpriority_2.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority_2 = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_3, + prioritiesarray_2^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontracks_2_2 = missiontracks_6; + prioritiesarray = 0^4; + indexpriority = 0; + newprioritiesarray = + [prioritiesarray with [indexpriority] = + missiontrackwithhighestpriority.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_2_2, + prioritiesarray^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontrackswithprio = + map<> prio_setpriorityinmissiontrackarray + <(prioritytracknumbers)>(missiontracks_6); + prioritytracknumbers = newprioritiesarray_4; + withouttracknb = missiontracks_2; + (withtracknumber, l81) = + mapfold<> calculatemissiontracknumber + <(Mctypes.kinitmissiontrackarray -> pre withtracknumber)>(withouttracknb, + 0 -> pre l81); + rdrtracks_2 = rdrtracks_3; + ifftracks_2 = ifftracks_3; + missiontracks_2 = mergedrdrtracks @ mergedifftracks; + (mergedrdrtracks, mergedifftracks) = + mapfold<> mc_tracks_fusion_onerdrwithifftracks + <()>(l140, l139); + l140 = + map<> convertrdrtracktomissiontrack + <()>(rdrtracks_2); + l139 = + map<> convertifftracktomissiontrack + <()>(ifftracks_2); + missiontracks_7 = missiontrackswithprio; + missiontracks_8 = missiontracks_7; + iffonoffcmd = iffonoffcmd_2; + rdrmodecmd = rdrmodecmd_2; + rdronoffcmd = rdronoffcmd_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) + (rdronoffcmd, rdrmodecmd, missiontracks_8, iffonoffcmd); + (l5, l6, l200) = (st, ifftracks_4, initializing); + (l201, l172, l3, l4) = (initializing_3, st_4, mode, rdrtracks_4) tel node dv_fighterdebug(res : bool; rdronoffclicked : bool; iffonoffclicked : bool) returns (proof3 : bool) -var missiontracks : Mctypes.tmissiontracksarray; l33 : bool; proof3_2 : bool; +var missiontracks_9 : Mctypes.tmissiontracksarray; l33 : bool; + proof3_2 : bool; res_2 : bool; rdronoffclicked_2 : bool; + iffonoffclicked_2 : bool; onoffcmd_4 : bool; modecmd_3 : bool; + failure_3 : bool; rdrdetectedtracks : Mctypes.tdetectedrdrtracksarray; + tracks_4 : Mctypes.ttracksarray; onoffcmd_2_3 : bool; failure_2_2 : bool; + x_2 : bool; initializing_2_2 : bool; st_3_2 : Mctypes.tsensorstate; + modecmd_2 : bool; mode_2 : Mctypes.trdrmode; + st_2_2 : Mctypes.tsensorstate; tracks_2_2 : Mctypes.ttracksarray; + rdrdetectedtracks_2 : Mctypes.tdetectedrdrtracksarray; + l22 : Mctypes.ttrack^Mctypes.ksizerdrtracksarray; + l30 : Mctypes.trdrtrack^Mctypes.ksizerdrtracksarray; + rdrtracks_2_2 : Mctypes.trdrtracksarray; initializing_3 : bool; + st_4 : Mctypes.tsensorstate; mode : Mctypes.trdrmode; + rdrtracks_4 : Mctypes.trdrtracksarray; tracks_3 : Mctypes.ttracksarray; + failure : bool; iffdetectedtracks : Mctypes.tdetectedifftracksarray; + onoffcmd_3 : bool; onoffcmd_2_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_2 : Mctypes.tifftracksarray; + st : Mctypes.tsensorstate; ifftracks_4 : 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; rdronoffbutton_2 : bool; + currentrdrstate_3 : Mctypes.tsensorstate; onoffbuttonpressed_2 : bool; + currentstate_3 : Mctypes.tsensorstate; onoffcmd_2 : bool; + re_Input_3 : bool; re_Output_3 : bool; rdronoffcmd_2 : bool; + currentrdrstate_2 : Mctypes.tsensorstate; rdrmodebutton_2 : bool; + currentrdrmode_2 : Mctypes.trdrmode; + currentstate_2 : Mctypes.tsensorstate; modebuttonpressed : bool; + currentmode : Mctypes.trdrmode; modecmd : bool; re_Input_2 : bool; + re_Output_2 : bool; rdrmodecmd_2 : bool; iffonoffbutton_2 : bool; + currentiffstate_2 : Mctypes.tsensorstate; onoffbuttonpressed : bool; + currentstate : Mctypes.tsensorstate; onoffcmd : bool; re_Input : bool; + re_Output : bool; iffonoffcmd_2 : bool; + rdrtracks_3 : Mctypes.trdrtracksarray; + ifftracks_3 : Mctypes.tifftracksarray; + missiontracks_6 : Mctypes.tmissiontracksarray; + missiontracks_5 : Mctypes.tmissiontracksarray; + prioritiesarray_4 : Mctypes.tpriorityList; indexpriority_4 : int; + missiontrackwithhighestpriority_4 : Mctypes.tmissiontrack; + newprioritiesarray_4 : Mctypes.tpriorityList; + missiontracks_4 : Mctypes.tmissiontracksarray; + prioritiesarray_3 : Mctypes.tpriorityList; indexpriority_3 : int; + missiontrackwithhighestpriority_3 : Mctypes.tmissiontrack; + newprioritiesarray_3 : Mctypes.tpriorityList; + missiontracks_3 : Mctypes.tmissiontracksarray; + prioritiesarray_2 : Mctypes.tpriorityList; indexpriority_2 : int; + missiontrackwithhighestpriority_2 : Mctypes.tmissiontrack; + newprioritiesarray_2 : Mctypes.tpriorityList; + missiontracks_2_2 : Mctypes.tmissiontracksarray; + prioritiesarray : Mctypes.tpriorityList; indexpriority : int; + missiontrackwithhighestpriority : Mctypes.tmissiontrack; + newprioritiesarray : Mctypes.tpriorityList; + prioritytracknumbers : Mctypes.tpriorityList; + missiontrackswithprio : Mctypes.tmissiontracksarray; + withouttracknb : Mctypes.tmissiontracksarray; l81 : int; + withtracknumber : Mctypes.tmissiontracksarray; + rdrtracks_2 : Mctypes.trdrtracksarray; + ifftracks_2 : Mctypes.tifftracksarray; + mergedrdrtracks : Mctypes.tmissiontrack^Mctypes.ksizerdrtracksarray; + mergedifftracks : Mctypes.tmissiontrack^Mctypes.ksizeifftracksarray; + l140 : Mctypes.tmissiontrack^Mctypes.ksizerdrtracksarray; + l139 : Mctypes.tmissiontrack^Mctypes.ksizeifftracksarray; + missiontracks_2 : Mctypes.tmissiontracksarray; + missiontracks_7 : Mctypes.tmissiontracksarray; rdronoffcmd : bool; + rdrmodecmd : bool; missiontracks_8 : Mctypes.tmissiontracksarray; + iffonoffcmd : bool; 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; + missiontracks : Mctypes.tmissiontracksarray; let - missiontracks = fighterdebug(res, rdronoffclicked, iffonoffclicked); + missiontracks_9 = missiontracks; l33 = fold<> dv_tracknumberexist - <()>(missiontracks, missiontracks^Mctypes.ksizemissiontracksarray, + <()>(missiontracks_9, missiontracks_9^Mctypes.ksizemissiontracksarray, false); proof3_2 = not(l33); - proof3 = dv_proof3(fighterdebug(res, rdronoffclicked, iffonoffclicked)) + res_2 = res; + rdronoffclicked_2 = rdronoffclicked; + iffonoffclicked_2 = iffonoffclicked; + onoffcmd_4 = false -> pre l10; + modecmd_3 = false -> pre l11; + failure_3 = false; + rdrdetectedtracks = [0, 1, 2, 3, 4]; + tracks_4 = l179; + onoffcmd_2_3 = onoffcmd_4; + failure_2_2 = failure_3; + initializing_2_2 = (&)((=)(st_3_2, Mctypes.TState_OFF), onoffcmd_2_3); + x_2 = false fby false fby false fby false fby false fby onoffcmd_2_3; + st_3_2 = + if failure_2_2 + then Mctypes.TState_FAIL + else if if onoffcmd_2_3 then x_2 else false + then Mctypes.TState_ON + else Mctypes.TState_OFF + ; + modecmd_2 = modecmd_3; + mode_2 = + if modecmd_2 then Mctypes.TRdrMode_NARROW else Mctypes.TRdrMode_WIDE; + st_2_2 = st_4; + tracks_2_2 = tracks_4; + rdrdetectedtracks_2 = rdrdetectedtracks; + rdrtracks_2_2 = + if (=)(st_2_2, Mctypes.TState_ON) + then l30 + else Mctypes.kinitrdrtrackarray; + l30 = map<> elaboraterdrtrack<()>(l22); + l22 = + map<> selectdetectedtrack + <()>(rdrdetectedtracks_2, tracks_2_2^Mctypes.ksizerdrtracksarray, + Mctypes.kinittrack^Mctypes.ksizerdrtracksarray); + rdrtracks_4 = rdrtracks_2_2; + mode = mode_2; + (initializing_3, st_4) = (initializing_2_2, st_3_2); + tracks_3 = l179; + failure = false; + iffdetectedtracks = [1, 2, 3]; + onoffcmd_3 = false -> pre l12; + onoffcmd_2_2 = onoffcmd_3; + failure_2 = failure; + initializing_2 = (&)((=)(st_3, Mctypes.TState_OFF), onoffcmd_2_2); + x = false fby false fby false fby false fby false fby onoffcmd_2_2; + st_3 = + if failure_2 + then Mctypes.TState_FAIL + else if if onoffcmd_2_2 then x else false + then Mctypes.TState_ON + else Mctypes.TState_OFF + ; + st_2 = st; + tracks_2 = tracks_3; + iffdetectedtracks_2 = iffdetectedtracks; + l34 = + map<> selectdetectedtrack + <()>(iffdetectedtracks_2, tracks_2^Mctypes.ksizeifftracksarray, + Mctypes.kinittrack^Mctypes.ksizeifftracksarray); + l40 = map<> ifftrack_of_track<()>(l34); + ifftracks_2_2 = + if (=)(st_2, Mctypes.TState_ON) then l40 else Mctypes.kinitifftrackarray; + ifftracks_4 = ifftracks_2_2; + (initializing, st) = (initializing_2, st_3); + currentrdrstate = l172; + currentrdrmode = l3; + rdrtracks = l4; + rdronoffbutton = rdronoffclicked_2; + rdrmodebutton = false; + iffonoffbutton = iffonoffclicked_2; + currentiffstate = l5; + ifftracks = l6; + rdronoffbutton_2 = rdronoffbutton; + currentrdrstate_3 = currentrdrstate; + onoffbuttonpressed_2 = re_Output_3; + currentstate_3 = currentrdrstate_3; + automaton + state Off + do + onoffcmd_2 = false + unless + | (&)(onoffbuttonpressed_2, (=)(currentstate_3, Mctypes.TState_OFF)) then On + state On + do + onoffcmd_2 = true + unless + | (&)(onoffbuttonpressed_2, (=)(currentstate_3, Mctypes.TState_ON)) then Off + end; + re_Input_3 = rdronoffbutton_2; + re_Output_3 = (&)(not(re_Input_3 -> pre re_Input_3), re_Input_3); + rdronoffcmd_2 = onoffcmd_2; + currentrdrstate_2 = currentrdrstate; + rdrmodebutton_2 = rdrmodebutton; + currentrdrmode_2 = currentrdrmode; + currentstate_2 = currentrdrstate_2; + modebuttonpressed = re_Output_2; + currentmode = currentrdrmode_2; + automaton + state Wide + do + modecmd = false + unless + | (&) + (modebuttonpressed, + (&) + ((=)(currentstate_2, Mctypes.TState_ON), + (=)(currentmode, Mctypes.TRdrMode_WIDE))) + then Narrow + state Narrow + do + modecmd = true + unless + | (&) + (modebuttonpressed, + (&) + ((=)(currentstate_2, Mctypes.TState_ON), + (=)(currentmode, Mctypes.TRdrMode_NARROW))) + then Wide + end; + re_Input_2 = rdrmodebutton_2; + re_Output_2 = (&)(not(re_Input_2 -> pre re_Input_2), re_Input_2); + rdrmodecmd_2 = modecmd; + iffonoffbutton_2 = iffonoffbutton; + currentiffstate_2 = currentiffstate; + onoffbuttonpressed = re_Output; + currentstate = currentiffstate_2; + 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; + re_Input = iffonoffbutton_2; + re_Output = (&)(not(re_Input -> pre re_Input), re_Input); + iffonoffcmd_2 = onoffcmd; + rdrtracks_3 = rdrtracks; + ifftracks_3 = ifftracks; + missiontracks_6 = withtracknumber; + missiontracks_5 = missiontracks_6; + prioritiesarray_4 = newprioritiesarray_3; + indexpriority_4 = 3; + newprioritiesarray_4 = + [prioritiesarray_4 with [indexpriority_4] = + missiontrackwithhighestpriority_4.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority_4 = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_5, + prioritiesarray_4^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontracks_4 = missiontracks_6; + prioritiesarray_3 = newprioritiesarray_2; + indexpriority_3 = 2; + newprioritiesarray_3 = + [prioritiesarray_3 with [indexpriority_3] = + missiontrackwithhighestpriority_3.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority_3 = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_4, + prioritiesarray_3^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontracks_3 = missiontracks_6; + prioritiesarray_2 = newprioritiesarray; + indexpriority_2 = 1; + newprioritiesarray_2 = + [prioritiesarray_2 with [indexpriority_2] = + missiontrackwithhighestpriority_2.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority_2 = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_3, + prioritiesarray_2^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontracks_2_2 = missiontracks_6; + prioritiesarray = 0^4; + indexpriority = 0; + newprioritiesarray = + [prioritiesarray with [indexpriority] = + missiontrackwithhighestpriority.Mctypes.m_tracknumber]; + missiontrackwithhighestpriority = + fold<> prio_selecthighestprioritynotinpriorityarray + <()>(missiontracks_2_2, + prioritiesarray^Mctypes.ksizemissiontracksarray, + Mctypes.kinitmissiontrack); + missiontrackswithprio = + map<> prio_setpriorityinmissiontrackarray + <(prioritytracknumbers)>(missiontracks_6); + prioritytracknumbers = newprioritiesarray_4; + withouttracknb = missiontracks_2; + (withtracknumber, l81) = + mapfold<> calculatemissiontracknumber + <(Mctypes.kinitmissiontrackarray -> pre withtracknumber)>(withouttracknb, + 0 -> pre l81); + rdrtracks_2 = rdrtracks_3; + ifftracks_2 = ifftracks_3; + missiontracks_2 = mergedrdrtracks @ mergedifftracks; + (mergedrdrtracks, mergedifftracks) = + mapfold<> mc_tracks_fusion_onerdrwithifftracks + <()>(l140, l139); + l140 = + map<> convertrdrtracktomissiontrack + <()>(rdrtracks_2); + l139 = + map<> convertifftracktomissiontrack + <()>(ifftracks_2); + missiontracks_7 = missiontrackswithprio; + missiontracks_8 = missiontracks_7; + iffonoffcmd = iffonoffcmd_2; + rdrmodecmd = rdrmodecmd_2; + rdronoffcmd = rdronoffcmd_2; + l179 = createalltracks(res_2); + (l10, l11, missiontracks, l12) = + (rdronoffcmd, rdrmodecmd, missiontracks_8, iffonoffcmd); + (l5, l6, l200) = (st, ifftracks_4, initializing); + (l201, l172, l3, l4) = (initializing_3, st_4, mode, rdrtracks_4); + proof3 = proof3_2 tel node dv_debug(missiontracks : Mctypes.tmissiontracksarray) @@ -1523,5 +2792,5 @@ let <()>(missiontracks_2, missiontracks_2^Mctypes.ksizemissiontracksarray, false); proof3_2 = not(l33); - proof3 = dv_proof3(missiontracks) + proof3 = proof3_2 tel