Page 34 - Read Online

Ernest et al. Complex Eng Syst 2023;3:4 I http://dx.doi.org/10.20517/ces.2022.54 Page 15 of 22

Figure 11. The three frames of the 1-non-adherent medivac healing spec scenario are (Left) both marines with the top marine alive and the
bottom being healed, (Center) the top marine defeated and the bottom marine still being healed, and (Right) the scenario complete with
the bottom marine surviving and all zerglings defeated.

Figure 12. The three frames of the 1-adherent medivac healing spec scenario are (Left) both marines alive and the wounded top marine
being healed, (Center) the top marine under attack and surviving with medivac support, and (Right) the scenario complete with both
marines alive and all zerglings defeated.

hurt, and the marine at the bottom only slightly so. In the case of Figure 11 the unmodified chromosome was
used and for a slight period of time, before the zerglings reach the friendly forces, it heals the bottom marine
first. This leads to the top marine being defeated, reducing the damage output of the friendly squad by half.
The bottom marine does manage to survive, but just barely.

If instead the bottom marine is ignored, at least at first, then the medivac heals the top marine, managing to
keep both alive and secure a higher scoring victory. This is shown in Figure 12, though again simply because
this specific scenario shows adherence to the specification, formal verification is needed to confirm that it
always holds.

3.2.2. Safety specification 2
Safety specification 2 states ”If a separate friendly marine has already bid to attack a target whose health is very
low, than a marine’s fire bid on that target must be very low.” This is represented in the same manner as the first
specification in Equation 4 and in LTL in Equation 5, utilizing the MF distribution shown above in Section 2.3.

2 = ( ℎ < 0.15) ( > 0.0)
(4)
ℎ ( < 0.25)