project_task_sheets/phase_00/project_phase00_tasks/Makefile

@@ -4,7 +4,7 @@ name = MichaelChen
 
 solutionname = Solution_Phase$(phase)_$(name)
 target = $(solutionname)_V$(version).zip
-package = $(solutionname).pdf PlayerTest.java
+package = $(solutionname).pdf
 latexmkflags =
 
 .PHONY : all dev

project_task_sheets/phase_00/project_phase00_tasks/PlayerTest.java

@@ -1,79 +0,0 @@
-package nl.tudelft.jpacman.level;
-
-import org.junit.jupiter.api.BeforeEach;
-import org.junit.jupiter.api.Test;
-
-import com.google.common.collect.Lists;
-
-import nl.tudelft.jpacman.board.Board;
-import nl.tudelft.jpacman.board.BoardFactory;
-import nl.tudelft.jpacman.board.Direction;
-import nl.tudelft.jpacman.board.Square;
-import nl.tudelft.jpacman.game.Game;
-import nl.tudelft.jpacman.game.GameFactory;
-import nl.tudelft.jpacman.npc.ghost.GhostFactory;
-import nl.tudelft.jpacman.sprite.PacManSprites;
-
-import static org.assertj.core.api.Assertions.assertThat;
-
-/**
- * Test suite to confirm the correct behaviour of pellet consumtion as
- * described in Scenario S2.1.
- *
- * @author Michael Chen
- */
-class PlayerTest {
-    private MapParser parser;
-    private GameFactory gameFact;
-
-    /**
-     * Prepare the game factory
-     */
-    @BeforeEach
-    void setUpTest() {
-        PacManSprites sprites = new PacManSprites();
-        parser = new MapParser(new LevelFactory(sprites,
-                new GhostFactory(sprites)), new BoardFactory(sprites));
-        gameFact = new GameFactory(new PlayerFactory(sprites));
-    }
-
-    /**
-     * Scenario S2.1: The player consumes
-     */
-    @Test
-    void playerConsumeTest() {
-        Level level = parser.parseMap(
-            Lists.newArrayList("####", "#P.#", "####"));
-        Board board = level.getBoard();
-        Game game = gameFact.createSinglePlayerGame(level);
-        Player player = game.getPlayers().get(0);
-        Square playerStart =  board.squareAt(1, 1);
-        Square pelletPos =  board.squareAt(2, 1);
-        
-        // Given the game has started,
-        game.start();
-        assertThat(game.isInProgress()).isTrue();
-        assertThat(player.getScore()).isZero();
-        
-        // and  my Pacman is next to a square containing a pellet;
-        assertThat(pelletPos.getOccupants())
-            .hasAtLeastOneElementOfType(Pellet.class);
-        assertThat(pelletPos.getOccupants()).hasSize(1);
-        Pellet pellet = (Pellet) pelletPos.getOccupants().get(0);
-        assertThat(playerStart.getOccupants()).contains(player);
-        
-        // When  I press an arrow key towards that square;
-        game.move(player, Direction.EAST);
-        
-        // Then  my Pacman can move to that square,
-        assertThat(pelletPos.getOccupants()).contains(player);
-        
-        // and  I earn the points for the pellet,
-        assertThat(player.getScore()).isEqualTo(pellet.getValue());
-        
-        // and  the pellet disappears from that square.
-        assertThat(pelletPos.getOccupants()).doesNotContain(pellet);
-        
-        game.stop();
-    }
-}

project_task_sheets/phase_00/project_phase00_tasks/Solution_Phase00_MichaelChen.tex

@@ -63,7 +63,7 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\def\name{Michael Chen}
+\def\name{[Add name here]}
 \def\group{\textit{Assigned in Phase 1}}
 
 \begin{document}
@@ -75,9 +75,7 @@
 \begin{question}{Learn to Understand given JUnit Tests}%[0]
   From the \texttt{src/test/java} folder, select 2 test files, and describe in your own words which parts of the system / program execution are tested, and which kind of failures may be targeted by these tests.
   \begin{answer}
-  The \texttt{nl.tudelft.jpacman.npc.ghost.NavigationTest} class contains 8 test cases that test the capabilities of the \texttt{Navigation} class which is used to navigate the 2D maps and find paths to specific squares or types of objects. There are several test cases that verify the correct behaviour of the navigator: it checks if the navigator can find a correct path between to spaces, it verifies the correct failure return value in case no path can be found, it verifies that nearby objects of specific types can be found and also that certain navigator objects (ghosts, players, null) will navigate terrain differently (null can pass through wall squares). Each test consists of three steps: the preparation step parses a map from a list of lines in the grid and creates the squares that shall be navigated or objects to be found, the execution step then runs the navigation module with the test parameters, and finally the assertion step verifies the correctness of the execution results.
+  [TODO: Add answer here]
-
-  The \texttt{nl.tudelft.jpacman.board.OccupantTest} class contains a couple of tests that verify the correct behaviour of the occupancy protocol of the squares and units. The game rules define a strict 0..1 to 0..1 relation between those objects: each square can be occupied by at most one unit and each unit can occupy at most one square at a time. The tests here check if the relationship \textbf{on both sides} is successfully established once the unit tries to occupy a square that is accessible to the unit. It also checks that the square can be safely occupied multiple times.
   \end{answer}
 \end{question}
 
@@ -87,9 +85,12 @@
 \begin{question}{Write your own JUnit Test}%[0]
   Inside the \texttt{src/test/java} folder, create a new test file "CustomTest.java", and write your own JUnit test for one scenario picked from "scenarios.md" (located in the \texttt{doc/} folder). The test is supposed to call the sequence of functions corresponding to the steps described in the chosen scenario, and should include reasonable \textit{assertions} to check if the intermediate program states meet the scenario requirements.
   \begin{answer}
-    I picked the scenarion \texttt{S2.1} to verify that the pellets are successfully consumed by the player once the player moves towards them.
+    [TODO: Add answer here]
 
-    \lstinputlisting[firstline=43,lastline=78,language=Java,belowskip=-0.8\baselineskip]{PlayerTest.java}
+    \begin{lstlisting}[language=Java,belowskip=-0.8\baselineskip]
+/* Add code here */
+    \end{lstlisting}
+    % or: \lstinputlisting[language=Java,belowskip=-0.8\baselineskip]{file_name.java}
   \end{answer}
 \end{question}
 

project_task_sheets/phase_05/project_phase05_tasks/DurationTest.java

@@ -1,45 +0,0 @@
-import org.junit.Assert;
-import org.junit.Test;
-
-public class DurationTest {
-    @Test
-    public void testToStringCORMutation() {
-        // Killed 4,5
-        Assert.assertEquals("PT-0.999999999S",
-            new Duration(-1, 1).toString());
-        // Killed 1,3,4,6,7
-        Assert.assertEquals("PT-1S",
-            new Duration(-1, 0).toString());
-        // Killed 1,3,4,6,8
-        Assert.assertEquals("PT0.000000001S",
-            new Duration(0, 1).toString());
-    }
-
-    @Test
-    public void testToStringRORMutation() {
-        // Killed Mutation: Line 18: Unequal
-        Assert.assertEquals("PT0S",
-            new Duration(0, 0).toString());
-        // Killed Mutation: Line 26: Equals, Line 35.1: Equals
-        Assert.assertEquals("PT-1S",
-            new Duration(-1, 0).toString());
-        // Killed Mutation: Line 29: Less
-        Assert.assertEquals("PT1M",
-            new Duration(60, 0).toString());
-        // Killed Mutation: Line 32.1: FalseOp, Line 32.2: Greater
-        Assert.assertEquals("PT0.000000001S",
-            new Duration(0, 1).toString());
-        // Killed Mutation: Line 35.2: Less
-        Assert.assertEquals("PT1.000000001S",
-            new Duration(1, 1).toString());
-        // Killed Mutation: Line 36: LessEquals
-        Assert.assertEquals("PT-58.999999999S",
-            new Duration(-59, 1).toString());
-        // Killed Mutation: Line 46: GreaterEquals
-        Assert.assertEquals("PT-0.999999999S",
-            new Duration(-1, 1).toString());
-        // Killed Mutation: Line 51: Unequal
-        Assert.assertEquals("PT0.0000001S",
-            new Duration(0, 100).toString());
-    }
-}

project_task_sheets/phase_05/project_phase05_tasks/Makefile

@@ -4,14 +4,14 @@ name = MichaelChen
 
 solutionname = Solution_Phase$(phase)_$(name)
 target = $(solutionname)_V$(version).zip
-package = $(solutionname).pdf Duration.java DurationTest.java build.xml mutation_test.bat mutants.txt Mutation_Testing_Sample_Model.xml
+package = $(solutionname).pdf Duration.java Mutation_Testing_Sample_Model.xml
 latexmkflags =
 
 .PHONY : all dev
 
 all : $(target)
 
-dev : latexmkflags = -pvc -interaction=nonstopmode
+dev : latexmkflags = -pvc
 dev : all
 
 $(target) : $(package)

project_task_sheets/phase_05/project_phase05_tasks/Mutation_Testing_Sample_Model.xml

@@ -1,13 +1,20 @@
 <?xml version="1.0" encoding="utf-8"?>
 <!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_2.dtd'>
 <nta>
-	<declaration>typedef int[47,58] char;
+	<declaration>// Place global declarations here.
-broadcast chan initialized;
 
-int c0_in = 0;
+                                           // As input to your method / class model, you can use either...
-int c1_in = 0;
+typedef int[-25,25] cust_t;                // ... a custom integer type which is restricted to a certain value range...
-int c2_in = 0;
+
-int c3_in = 0;</declaration>
+const int list_size = 4;                   // ...or a fixed number of given values...
+int values[list_size] = {-1, 0, 1, 300};   // ... which are defined in this array ...
+typedef int[0,list_size-1] index_t;        // ... and are indexed inside the model via this index type.
+
+broadcast chan initialized;                // The broadcast channel assures that the initial variable assignment in the method / class model is synchronized
+                                           // with the completion of the value generation (e.g. of InputFromRange or InputFromList)
+
+int x_in = 0;                              // These variables globally hold the initial input values to the method / class model
+int y_in = 0;</declaration>
 	<template>
 		<name>InputFromRange</name>
 		<location id="id0" x="-238" y="-204">
@@ -27,197 +34,195 @@ int c3_in = 0;</declaration>
 		<transition>
 			<source ref="id1"/>
 			<target ref="id2"/>
-			<label kind="select" x="-603" y="-297">c0_val : char,
+			<label kind="select" x="-637" y="-238">xi : cust_t, yi : cust_t</label>
-c1_val : char,
+			<label kind="assignment" x="-620" y="-187">x_in = xi, y_in = yi</label>
-c2_val : char,
-c3_val : char</label>
-			<label kind="assignment" x="-603" y="-187">c0_in = c0_val,
-c1_in = c1_val,
-c2_in = c2_val,
-c3_in = c3_val</label>
 		</transition>
 	</template>
 	<template>
-		<name x="5" y="5">Number</name>
+		<name>InputFromList</name>
-		<declaration>int c0 = 0;
+		<location id="id3" x="42" y="8">
-int c1 = 0;
+			<urgent/>
-int c2 = 0;
-int c3 = 0;
-
-int c = 0;</declaration>
-		<location id="id3" x="297" y="-34">
-			<name x="287" y="-68">End</name>
 		</location>
-		<location id="id4" x="51" y="-34">
+		<location id="id4" x="238" y="9">
-			<name x="8" y="-68">Branch</name>
 		</location>
-		<location id="id5" x="-161" y="-33">
+		<location id="id5" x="-195" y="8">
-			<name x="-171" y="-67">Init</name>
 			<urgent/>
 		</location>
 		<init ref="id5"/>
 		<transition>
-			<source ref="id4"/>
+			<source ref="id3"/>
-			<target ref="id3"/>
+			<target ref="id4"/>
-			<label kind="guard" x="102" y="-17">!(c0 &gt;= 48 &amp;&amp; c0 &lt;= 57
+			<label kind="synchronisation" x="94" y="-16">initialized!</label>
-&amp;&amp; c1 &gt;= 48 &amp;&amp; c1 &lt;= 57
-&amp;&amp; c2 &gt;= 48 &amp;&amp; c2 &lt;= 57
-&amp;&amp; c3 &gt;= 48 &amp;&amp; c3 &lt;= 57)</label>
-			<label kind="assignment" x="153" y="-68">c = -1</label>
-			<label kind="comments" x="195" y="-68">Invalid</label>
-		</transition>
-		<transition>
-			<source ref="id4"/>
-			<target ref="id3"/>
-			<label kind="guard" x="-8" y="-229">c0 &gt;= 48 &amp;&amp; c0 &lt;= 57
-&amp;&amp; c1 &gt;= 48 &amp;&amp; c1 &lt;= 57
-&amp;&amp; c2 &gt;= 48 &amp;&amp; c2 &lt;= 57
-&amp;&amp; c3 &gt;= 48 &amp;&amp; c3 &lt;= 57</label>
-			<label kind="assignment" x="229" y="-229">c = (c0 - 48) * 1000
-+ (c1 - 48) * 100
-+ (c2 - 48) * 10
-+ (c3 - 48)</label>
-			<label kind="comments" x="170" y="-221">Result</label>
-			<nail x="178" y="-170"/>
 		</transition>
 		<transition>
 			<source ref="id5"/>
-			<target ref="id4"/>
+			<target ref="id3"/>
-			<label kind="synchronisation" x="-102" y="-59">initialized?</label>
+			<label kind="select" x="-178" y="-25">ind_x : index_t, ind_y : index_t</label>
-			<label kind="assignment" x="-102" y="-17">c0 = c0_in,
+			<label kind="assignment" x="-204" y="26">x_in = values[ind_x], y_in = values[ind_y]</label>
-c1 = c1_in,
-c2 = c2_in,
-c3 = c3_in</label>
 		</transition>
 	</template>
 	<template>
-		<name x="5" y="5">NumberMutant</name>
+		<name x="5" y="5">SetEqual</name>
-		<declaration>int c0 = 0;
+		<declaration>// Place local declarations here.
-int c1 = 0;
+int x = 0;
-int c2 = 0;
+int y = 0;</declaration>
-int c3 = 0;
-
-int c = 0;</declaration>
 		<location id="id6" x="297" y="-34">
 			<name x="287" y="-68">End</name>
 		</location>
-		<location id="id7" x="51" y="-34">
+		<location id="id7" x="178" y="25">
-			<name x="8" y="-68">Branch</name>
+			<name x="168" y="-9">B</name>
 		</location>
-		<location id="id8" x="-161" y="-33">
+		<location id="id8" x="178" y="-102">
+			<name x="170" y="-85">A</name>
+		</location>
+		<location id="id9" x="51" y="-34">
+		</location>
+		<location id="id10" x="-161" y="-33">
 			<name x="-171" y="-67">Init</name>
 			<urgent/>
 		</location>
-		<init ref="id8"/>
+		<init ref="id10"/>
 		<transition>
 			<source ref="id7"/>
 			<target ref="id6"/>
-			<label kind="guard" x="102" y="-17">!(c0 &gt;= 48 &amp;&amp; c0 &lt;= 57
+			<label kind="guard" x="221" y="8">!(x&lt;y)</label>
-&amp;&amp; c1 &gt;= 48 &amp;&amp; c1 &lt;= 57
-&amp;&amp; c2 &gt;= 48 &amp;&amp; c2 &lt;= 57
-&amp;&amp; c3 &gt;= 48)</label>
-			<label kind="assignment" x="153" y="-68">c = -1</label>
-			<label kind="comments" x="195" y="-68">Invalid</label>
 		</transition>
 		<transition>
 			<source ref="id7"/>
-			<target ref="id6"/>
+			<target ref="id7"/>
-			<label kind="guard" x="-8" y="-229">c0 &gt;= 48 &amp;&amp; c0 &lt;= 57
+			<label kind="guard" x="161" y="68">x&lt;y</label>
-&amp;&amp; c1 &gt;= 48 &amp;&amp; c1 &lt;= 57
+			<label kind="assignment" x="161" y="102">x=x+1</label>
-&amp;&amp; c2 &gt;= 48 &amp;&amp; c2 &lt;= 57
+			<nail x="238" y="93"/>
-&amp;&amp; c3 &gt;= 48</label>
+			<nail x="102" y="93"/>
-			<label kind="assignment" x="229" y="-229">c = (c0 - 48) * 1000
-+ (c1 - 48) * 100
-+ (c2 - 48) * 10
-+ (c3 - 48)</label>
-			<label kind="comments" x="170" y="-221">Result</label>
-			<nail x="178" y="-170"/>
 		</transition>
 		<transition>
 			<source ref="id8"/>
-			<target ref="id7"/>
+			<target ref="id8"/>
-			<label kind="synchronisation" x="-102" y="-59">initialized?</label>
+			<label kind="guard" x="161" y="-204">x&gt;y</label>
-			<label kind="assignment" x="-102" y="-17">c0 = c0_in,
+			<label kind="assignment" x="153" y="-170">x=x-1</label>
-c1 = c1_in,
+			<nail x="246" y="-178"/>
-c2 = c2_in,
+			<nail x="93" y="-178"/>
-c3 = c3_in</label>
+		</transition>
+		<transition>
+			<source ref="id8"/>
+			<target ref="id6"/>
+			<label kind="guard" x="221" y="-93">!(x&gt;y)</label>
+		</transition>
+		<transition>
+			<source ref="id9"/>
+			<target ref="id7"/>
+			<label kind="guard" x="76" y="0">x&lt;y</label>
+		</transition>
+		<transition>
+			<source ref="id9"/>
+			<target ref="id8"/>
+			<label kind="guard" x="76" y="-93">x&gt;=y</label>
 		</transition>
-	</template>
-	<template>
-		<name x="5" y="5">NumberBranch</name>
-		<declaration>int c0 = 0;
-int c1 = 0;
-int c2 = 0;
-int c3 = 0;
-
-int c = 0;</declaration>
-		<location id="id9" x="297" y="-34">
-			<name x="287" y="-68">End</name>
-		</location>
-		<location id="id10" x="51" y="-34">
-			<name x="8" y="-68">Branch</name>
-		</location>
-		<location id="id11" x="-161" y="-33">
-			<name x="-171" y="-67">Init</name>
-			<urgent/>
-		</location>
-		<init ref="id11"/>
 		<transition>
 			<source ref="id10"/>
 			<target ref="id9"/>
-			<label kind="guard" x="102" y="-17">!(c0 &gt;= 48 &amp;&amp; c0 &lt;= 57
+			<label kind="synchronisation" x="-102" y="-59">initialized?</label>
-&amp;&amp; c1 &gt;= 48 &amp;&amp; c1 &lt;= 57
+			<label kind="assignment" x="-119" y="-25">x = x_in, y = y_in</label>
-&amp;&amp; c2 &gt;= 48 &amp;&amp; c2 &lt;= 57
-&amp;&amp; c3 &gt;= 48 &amp;&amp; c3 &lt;= 57)
-&amp;&amp; c == -2</label>
-			<label kind="assignment" x="153" y="-68">c = -1</label>
-			<label kind="comments" x="195" y="-68">Invalid</label>
 		</transition>
+	</template>
+	<template>
+		<name>SetEqualMutant</name>
+		<declaration>// Place local declarations here.
+int x = 0;
+int y = 0;</declaration>
+		<location id="id11" x="144" y="51">
+			<name x="134" y="17">B</name>
+		</location>
+		<location id="id12" x="263" y="-8">
+			<name x="253" y="-42">End</name>
+		</location>
+		<location id="id13" x="144" y="-76">
+			<name x="136" y="-59">A</name>
+		</location>
+		<location id="id14" x="17" y="-8">
+		</location>
+		<location id="id15" x="-195" y="-7">
+			<name x="-205" y="-41">Init</name>
+			<urgent/>
+		</location>
+		<init ref="id15"/>
 		<transition>
-			<source ref="id10"/>
+			<source ref="id14"/>
-			<target ref="id10"/>
+			<target ref="id12"/>
-			<label kind="guard" x="-8" y="-229">c0 &gt;= 48 &amp;&amp; c0 &lt;= 57
+			<label kind="guard" x="119" y="-34">x&gt;=y</label>
-&amp;&amp; c1 &gt;= 48 &amp;&amp; c1 &lt;= 57
-&amp;&amp; c2 &gt;= 48 &amp;&amp; c2 &lt;= 57
-&amp;&amp; c3 &gt;= 48 &amp;&amp; c3 &lt;= 57
-&amp;&amp; c == -2</label>
-			<label kind="assignment" x="229" y="-229">c = (c0 - 48) * 1000
-+ (c1 - 48) * 100
-+ (c2 - 48) * 10
-+ (c3 - 48)</label>
-			<label kind="comments" x="170" y="-221">Result</label>
-			<nail x="178" y="-170"/>
-			<nail x="221" y="-119"/>
 		</transition>
 		<transition>
 			<source ref="id11"/>
-			<target ref="id10"/>
+			<target ref="id12"/>
-			<label kind="synchronisation" x="-102" y="-59">initialized?</label>
+			<label kind="guard" x="187" y="34">!(x&lt;y)</label>
-			<label kind="assignment" x="-102" y="-17">c0 = c0_in,
+		</transition>
-c1 = c1_in,
+		<transition>
-c2 = c2_in,
+			<source ref="id11"/>
-c3 = c3_in,
+			<target ref="id11"/>
-c = -2</label>
+			<label kind="guard" x="127" y="94">x&lt;y</label>
+			<label kind="assignment" x="127" y="128">x=x+1</label>
+			<nail x="204" y="119"/>
+			<nail x="68" y="119"/>
+		</transition>
+		<transition>
+			<source ref="id13"/>
+			<target ref="id13"/>
+			<label kind="guard" x="127" y="-178">x&gt;y</label>
+			<label kind="assignment" x="119" y="-144">x=x-1</label>
+			<nail x="212" y="-152"/>
+			<nail x="59" y="-152"/>
+		</transition>
+		<transition>
+			<source ref="id13"/>
+			<target ref="id12"/>
+			<label kind="guard" x="187" y="-67">!(x&gt;y)</label>
+		</transition>
+		<transition>
+			<source ref="id14"/>
+			<target ref="id11"/>
+			<label kind="guard" x="42" y="26">x&lt;y</label>
+		</transition>
+		<transition>
+			<source ref="id15"/>
+			<target ref="id14"/>
+			<label kind="synchronisation" x="-136" y="-34">initialized?</label>
+			<label kind="assignment" x="-153" y="0">x = x_in, y = y_in</label>
 		</transition>
 	</template>
-	<system>NUM = Number();
+	<system>// Place template instantiations here.
-// NUM = NumberMutant(); // to test the expression mutation
-// NUM = NumberBranch(); // to test the branch mutation
-IN_RANGE = InputFromRange();
 
-system IN_RANGE, NUM;</system>
+SE = SetEqual();                // The instance of the original model
+SE_MUT = SetEqualMutant();      // The instance of the mutated model
+IN_RANGE = InputFromRange();    // Use this template in the system definition below if you want take input values from an integer range...
+IN_LIST = InputFromList();      // ...or this if you want to provide a predefined list of possible / probable / common input values
+
+// List one or more processes to be composed into a system.
+
+system IN_RANGE, SE, SE_MUT;</system>
 	<queries>
 		<query>
-			<formula>A[] NUM.End imply (NUM.c &gt;= -1 &amp;&amp; NUM.c &lt; 10000)</formula>
+			<formula>A[] (SE.End &amp;&amp; SE_MUT.End) imply (SE.x == SE_MUT.x &amp;&amp; SE.y == SE_MUT.y)
-			<comment>Return value of the function is always a 4 digit number or -1.</comment>
+			</formula>
+			<comment>This formula can be used to compare the results and/or states of the original and the mutated template. 
+In this example, it covers the requirement that for all paths (A), all states on that individual path ([]) should satisfy that if the locations "SE.End" and "SE_MUT.End" are active (meaning that both instances reached the final state), 
+the x and y values of the original model template should be equal to the corresponding values of the mutated template.
+(Note: "SE.End" represents the "End" location of the template instance for the method / class as named in the "System declarations" section)
+			</comment>
 		</query>
 		<query>
-			<formula>A[] not deadlock || NUM.End</formula>
+			<formula>A[] SE.End imply (SE.x == SE.y)
-			<comment>Model never deadlocks and always reaches the end location.</comment>
+			</formula>
+			<comment>This formula covers the requirement that for all paths (A), all states on that individual path ([]) should satisfy that if the location "SE.End" is active, the x and y values of that template instance (SE.x, SE.y) must be equal.
+(Note: "SE.End" represents the "End" location of the template instance for the method / class as named in the "System declarations" section)
+			</comment>
 		</query>
 		<query>
-			<formula>A[] (NUM.End imply (NUM.c1 == 48 &amp;&amp; NUM.c1 == 49 &amp;&amp; NUM.c2 == 50 &amp;&amp; NUM.c3 == 51 imply NUM.c == 1234))</formula>
+			<formula>A[] SE.End imply (SE.y == y_in)
-			<comment>Simple test case.</comment>
+			</formula>
+			<comment>This formula covers the requirement that for all paths (A), all states on that individual path ([]) should satisfy that if the location "SE.End" is active, the y value of the template instance (SE.y) must still be equal to the input value y_in. 
+Of course, you can even be more strict with this property, and adapt it so that "SE.y" should remain unchanged in every single state along the algorithm execution.
+(Note: "SE.End" represents the "End" location of the template instance for the method / class as named in the "System declarations" section)
+			</comment>
 		</query>
 	</queries>
 </nta>

project_task_sheets/phase_05/project_phase05_tasks/Solution_Phase05_MichaelChen.tex

@@ -5,17 +5,6 @@
 \usepackage{listings}
 \usepackage{enumitem}
 \usepackage{subcaption}
-\usepackage[acronym]{glossaries}
-
-\newacronym{bnf}{BNF}{Backus-Naur form}
-\newacronym{fsm}{FSM}{finite state machine}
-\newacronym{tsc}{TSC}{terminal symbol coverage}
-\newacronym{pdc}{PDC}{production coverage}
-\newacronym{dc}{DC}{derivation coverage}
-\newacronym{moc}{MOC}{mutation operator coverage}
-\newacronym{mpc}{MPC}{mutation production coverage}
-\newacronym{wmc}{WMC}{weak mutant coverage}
-\newacronym{smc}{SMC}{strong mutant coverage}
 
 \usepackage{pgf}
 \usepackage{tikz}
@@ -74,8 +63,8 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\def\name{Michael Chen}
+\def\name{[Add name here]}
-\def\group{Group 01 (fastjson)}
+\def\group{[Add group here]}
 
 \begin{document}
 \projectinfo{5}{Software Testing - Syntax Coverage\small}{\today}{\name}{\group}
@@ -90,57 +79,32 @@
     \begin{enumerate}
       \item \textit{Production Rule}, \textit{Generator}, and \textit{Terminal}
       \begin{answer}
-      A Grammar is a set of \textit{words} or, as called here, \textit{strings}, that it accepts. Grammars can be described in different ways such as set notation, regular expressions, or in \gls{bnf}. \Gls{bnf} is set of production rules, also called rewrite rules, that map a set of symbols to a single symbol which is the name of the production rule. Symbols can be either non-terminals which represent non-trivial sytactic constructs such as loops or declarations in programming, while terminal symbols represent tokens, such as integer or string literals in programming languages. A generator is a \gls{fsm} that, given a grammar in \gls{bnf}, can generate a word of the grammar by recursively applying productions on the starting symbol until the syntax tree's leafs are only terminal symbols.
+      [TODO: Add answer here]
       \end{answer}
 
       \item \textit{Mutant}, \textit{Ground String}, and \textit{Mutation Operator}
       \begin{answer}
-      A ground string is a string that is accepted by a grammar. In other terms it is a string where we already know that a proof exists, that shows the string is in the grammar (ground truth). We can now change this string a little bit by applying specific rules, called mutation operators, that generate new strings that may or may not be accepted by the grammar, called mutants.
+      [TODO: Add answer here]
       \end{answer}
 
         \item \textit{RIP Model}
         \begin{answer}
-      The RIP model declares three requirements that are fulfilled when a failure occurrs. If all three of these are true, only then a failure can be detected. Firstly, the location of the fault in the code must be reached (\textbf{Reachability}), then, the program's internal state must be corrupted, i.e. an error occurred (\textbf{Infection}) and, finally, the error must have propagated to the program's output where the failure can then be observed (\textbf{Propagation}).
+        [TODO: Add answer here]
         \end{answer}
     \end{enumerate}
     \item Name and describe \textit{2 syntax-based coverage criteria}. Does one of these two criteria subsume the other? Explain why, or provide a counterexample.
     \begin{answer}
-    Two criteria on mutation operators are \gls{moc} and \gls{mpc}. \Gls{moc} introduces test requirements for every mutation operator, where the test is applied to the mutant created by the operator. This is trivially subsumed by the \gls{mpc}, which in addition to that, requires that for every production in the grammar, which the operator is applicable to, a test requirement is added.
+    [TODO: Add answer here]
     \end{answer}
 
     \item What does it mean to \textit{"kill a mutant"}? Explain the concept with an own code example.
     \begin{answer}
-    A test (strongly) kills a mutant if all three conditions of the RIP model are satisfied for it's test execution. Consider the following mutated \texttt{max} program:
+    [TODO: Add answer here]
-    \begin{lstlisting}[language=C]
-    int max(int a, int b) {
-      // return a > b ? a : b; // original
-      return a < b ? a : b; // mutant
-    }
-    \end{lstlisting}
-
-    A test that kills this mutant could be the following:
-    \begin{lstlisting}[language=C]
-    void kill_max_mutation() {
-      assert(max(1, 3) == 3);
-    }
-    \end{lstlisting}
-
-    \begin{enumerate}
-      \item This test satisfies the reachability requirement trivially.
-      \item The program is infected because the changed operator causes the program to select the wrong branch of the ternary expression.
-      \item And finally the error propagated to the function output, in this case also trivially because the incorrect value is directly returned.
-    \end{enumerate}
-    Because the RIP model is satisfied the mutation is successfully killed by the test.
     \end{answer}
 
     \item Name and describe the \textit{4 different classified types} of mutants in the context of mutant killing.
     \begin{answer}
-    \begin{itemize}
+    [TODO: Add answer here]
-      \item \textbf{Dead mutants} have been successfully killed by a test case.
-      \item \textbf{Trivial mutants} are killed by any any test case in that the variation is so severe, that the program will almost certainly result in a failure.
-      \item \textbf{Stillborn mutants} cannot be killed by any test case because they are syntactically illegal, i.e. cannot be executed.
-      \item \textbf{Equivalent mutants} can also not be killed, because the mutation does not cause the program to behave differently.
-    \end{itemize}
     \end{answer}
 
 \end{enumerate}
@@ -154,108 +118,37 @@
 
     \item Select \textit{one} mutation operator from Table~\ref{table:operators} (the operators are taken from \textit{Introduction to Software Testing} by Ammann and Offutt), and apply it \textit{once} to every occurrence of a target expression, statement or instruction inside the given \texttt{toString()} method (e.g., choose the \textit{SOR} operator, and for each \verb|<<|, \verb|>>|, or \verb|>>>| that occurs in the method, replace it with \textit{one} other shift operator). The operator has to be applicable to at least two parts of the code. For each mutation, document the line, original epression, and mutated expression.
     \begin{answer}
-    Here are the applications of the mutation operator ROR. All the mutation rules you have provided in Table~\ref{table:operators} differ from the definitions in \textit{Introduction to Software Testing} by Ammann and Offutt. The textbook definition requires all operators to be replaced by all other operators (and \textit{trueOp} and \textit{falseOp}), whereas your formal definition only requires the \verb|>| to be replaced (see left side of the production). Even though your definition is not precisely correct i have listed the missing mutations to the textbook definition in the lower part of the table.
+    [TODO: Add answer here]
-    \begin{center}
-    \begin{tabular}{r|c|c}
-      Line & Ground String & Mutant \\ \hline \hline
-      32 & \verb|buf.length() > 2| & \verb|buf.length() != 2| \\
-      35 & \verb|nanos > 0| & \verb|nanos < 0| \\
-      44 & \verb|nanos > 0| & \verb|true| \\ \hline
-      18 & \verb|this == ZERO|  & \verb|this != ZERO| \\
-      26 & \verb|hours != 0| & \verb|hours == 0| \\
-      29 & \verb|minutes != 0| & \verb|minutes < 0| \\
-      32 & \verb|secs == 0| & \verb|false| \\
-      32 & \verb|nanos == 0| & \verb|nanos > 0| \\
-      35 & \verb|secs < 0| & \verb|secs == 0| \\
-      36 & \verb|secs == -1| & \verb|secs <= -1| \\
-      46 & \verb|secs < 0| & \verb|secs >= 0| \\
-      51 & \verb|lastChar(buf) == '0'| & \verb|lastChar(buf) != '0'|
-    \end{tabular}
-    \end{center}
     \end{answer}
 
     \item Select \textit{one} other mutation operator, and apply all of its concrete mutations to \textit{one} target expression, statement or instruction inside the given \texttt{toString()} method (e.g., choose the \textit{SOR} operator, and replace one occurring \verb|<<| with the other shift operators \verb|>>| and \verb|>>>|). Document the line, original epression, and mutated expressions.
     \begin{answer}
-    The predicate \verb|secs < 0 && nanos > 0| in line~35 results in the following mutations when applying COR:
+    [TODO: Add answer here]
-    \begin{enumerate}
-      \item \verb+secs < 0 || nanos > 0+
-      \item \verb+secs < 0 & nanos > 0+
-      \item \verb+secs < 0 | nanos > 0+
-      \item \verb+secs < 0 ^ nanos > 0+
-      \item \verb+false+
-      \item \verb+true+
-      \item \verb+secs < 0+
-      \item \verb+nanos > 0+
-    \end{enumerate}
     \end{answer}
 
     \item Pick one set of method mutations (either the mutations of task 2a or 2b), and provide a minimum set of tests that kill all introduced mutants \textit{strongly} (\textit{Strong Mutation Coverage (SMC)}). If that is not possible for a concrete mutant, explain why, and kill that mutant \textit{weakly} (\textit{Weak Mutation Coverage (WMC)}) instead. If neither of that is possible, explain it as well.
     \begin{answer}
-    The following test case kills all mutations from the COR set from task~2b except the second mutation, because for boolean values the \verb|&| operator is similar to the \verb|&&| operator, thus we have an equivalent mutant.
+    [TODO: Add answer here]
 
-    \lstinputlisting[language=Java,firstline=5,lastline=16,belowskip=-0.8\baselineskip]{DurationTest.java}
+    \begin{lstlisting}[language=Java,belowskip=-0.8\baselineskip]
+/* Add code here */
+    \end{lstlisting}
+    % or: \lstinputlisting[language=Java,belowskip=-0.8\baselineskip]{file_name.java}
     \end{answer}
 
     \item For the \textit{other} set of method mutations, provide a minimum set of tests that kill the mutants only \textit{weakly}, but \textbf{not} \textit{strongly}. If that is not possible for a concrete mutant, explain why, and kill the mutants \textit{strongly} instead. If that is not possible as well, explain it.
     \begin{answer}
-    The mutant in line 32 \verb|buf.length() != 2| cannot be killed because the effect of the unequal operation in the context of buffer length is equal to the strictly greater than, because the buffer is always prefixed with \texttt{PT}. Of the remaining mutants, the following cannot be weakly killed (note, that all of those were optional as per your ROR definition):
+    [TODO: Add answer here]
-    \begin{center}
-    \begin{tabular}{r|c|l}
-      Line & Ground String & Mutant \\ \hline \hline
-      26 & \verb|hours != 0| & \verb|hours == 0| \\
-      29 & \verb|minutes != 0| & \verb|minutes < 0| \\
-      36 & \verb|secs == -1| & \verb|secs <= -1| \\
-      46 & \verb|secs < 0| & \verb|secs >= 0| \\
-      51 & \verb|lastChar(buf) == '0'| & \verb|lastChar(buf) != '0'|
-    \end{tabular}
-    \end{center}
-    Most of them are not weakly killable for the same reason: if the line is reached and infection is observed during execution, it will \textbf{always} cause the control flow to change into another branch and infect the string builder buffer. Except for the mutant in line~51, where in addition an infection will likely cause IndexOutOfRangeExceptions for the following decimal point insertion in line~54.
 
-    \lstinputlisting[language=Java,firstline=18,lastline=44,belowskip=-0.8\baselineskip]{DurationTest.java}
+    \begin{lstlisting}[language=Java,belowskip=-0.8\baselineskip]
+/* Add code here */
+    \end{lstlisting}
+    % or: \lstinputlisting[language=Java,belowskip=-0.8\baselineskip]{file_name.java}
     \end{answer}
 
     \item For both applied operators, select one concrete mutation and describe the conditions that need to hold for the \textit{Reachability}, \textit{Infection}, and \textit{Propagation} of the induced change.
     \begin{answer}
-    \begin{itemize}
+    [TODO: Add answer here]
-      \item \verb+secs < 0 || nanos > 0+ mutation in line~35. In order for the control flow to reach this line the guard in line~32 must be false, which means, either the seconds (not total seconds) or nanoseconds are not zero and still have to be appended, or no hours and minutes have already been appended so we have to append seconds, regardless if they are zero or not. To infect this line we have to create a wrong output in the mutation:
-      \begin{center}
-      \begin{tabular}{c|c||c|c|c}
-        \verb+secs < 0+ & \verb+nanos > 0+ & \verb+&&+ & \verb+||+ & Infected \\ \hline \hline
-        F & F & F & F & F \\
-        F & T & F & T & T \\
-        T & F & F & T & T \\
-        T & T & T & T & F
-      \end{tabular}
-      \end{center}
-      So, in order to infect the line we have have to make sure exactly one of the conditions from the above table is true. In this case the error will always propagate because in case of infection the buffer will be changed \textbf{or} returned immediately.
-
-      The conditions for the RIP model are as follows:
-      \begin{itemize}
-        \item \textbf{Reachability:} $\texttt{secs} \neq 0 \lor \texttt{nanos} \neq 0 \lor (\texttt{hours} = 0 \land \texttt{minutes} = 0)$
-        \item \textbf{Infection:} $\texttt{secs} < 0 \oplus \texttt{nanos} > 0$
-        \item \textbf{Propagation:} $\top$
-      \end{itemize}
-
-      \item \verb+nanos < 0+ in line~35. Reachability is similar to the above (here I am conforming to what we discussed in a previous exercise, where I was told to ignore boolean short circuiting on high-level language view and I will only consider predicate logic). Reachability is similar to the above example, because the source code line is the same.
-      \begin{center}
-      \begin{tabular}{c||c|c|c}
-        \texttt{nanos} & \verb+nanos < 0+ & \verb+nanos > 0+ & Infected \\ \hline \hline
-        0 & F & F & F \\
-        positive & F & T & T \\
-        negative & T & F & T
-      \end{tabular}
-      \end{center}
-      There are only three possible combinations of truth values for the infection matrix, because it is not possible for both to be true at the same time. So infection will always happen if the \texttt{nanos} are non-zero.
-
-      The only possible propagation method for this predicate is the branch in line~35 that is indirectly decided by the mutated statement. If the seconds are negative the branch is directly decided by the infection. If the seconds are non-negative the infection does not change the outcome of the branch predicate and will not propagate.
-
-      The conditions for the RIP model are as follows:
-      \begin{itemize}
-        \item \textbf{Reachability:} $\texttt{secs} \neq 0 \lor \texttt{nanos} \neq 0 \lor (\texttt{hours} = 0 \land \texttt{minutes} = 0)$
-        \item \textbf{Infection:} $\texttt{nanos} \neq 0$
-        \item \textbf{Propagation:} $\texttt{secs} < 0$
-      \end{itemize}
-    \end{itemize}
     \end{answer}
 
     \begin{table}[t]
@@ -291,86 +184,42 @@
 
     \item As a group, decide on \textbf{one test suite} (original + own tests) that you want to use for this task
     \begin{answer}
-    The current head of the \texttt{develop} branch will be used by our group to test our project.
+    [TODO: Add answer here]
     \end{answer}
 
     \item In consultation with your group, pick a unique mutation tool for Java code (i.e., no two members of one group should use the same tool).
     \begin{answer}
-    I picked the Major mutation tool for testing our project. Note that, because the mutation testing tool does not integrate well with Junit we have to create an additional test driver class that manually runs the Junit tests. Because of this manual effort I restrict the test to the \texttt{JSONScanner} class and mutation testing to its \texttt{checkTime} function that I have been developing tests for in the previous exercise.
+    [TODO: Add answer here]
     \end{answer}
 
     \item Depending on the capabilities of the selected mutation testing tool, determine the amount of \textit{killed mutants} for at least \textbf{3 different mutation operators} (handle the results individually as long as your tool returns the results for each individual operator, or supports the application of single selected operators).
     \begin{answer}
-    For the method under test the major tool generated a mutated class with 6239 mutations, 112 of those in the \texttt{checkTime} function. For this method the tool managed to create 28 COR mutations, 11 LVR mutations, 63 ROR mutations and 10 STD mutations. I did not manage to analyze the mutations that were killed. This is probably due to incompatible build tools (Major uses Java 1.7 while fastjson uses Java 1.5). For this reason I took the mutations from the generated log (attached as file \texttt{mutants.txt}) and for all 4 applicable mutation operators in the method under test manually edited the Java file and ran the test suite. The result can be seen in the below table:
+    [TODO: Add answer here]
-
-
-    \begin{center}
-    \begin{tabular}{c|c|c|c|c}
-    Operator & Line & Original & Mutation & Killed \\ \hline \hline
-    ROR & 729 & \verb+h0 == '0'+ & \verb+h0 <= '0'+ & live \\ % ID: 2275
-    ROR & 729 & \verb+h0 == '0'+ & \verb+h0 >= '0'+ & killed \\ % ID: 2276
-    ROR & 729 & \verb+h0 == '0'+ & \verb+false+ & killed \\ % ID: 2277
-    ROR & 730 & \verb+h1 < '0'+ & \verb+h1 != '0'+ & killed \\ % ID: 2278
-    ROR & 730 & \verb+h1 < '0'+ & \verb+h1 <= '0'+ & live \\ % ID: 2279
-    COR & 730 & \verb+h1 < '0' || h1 > '9'+ & \verb+h1 < '0' != h1 > '9'+ & live \\ % ID: 2284
-    COR & 730 & \verb+h1 < '0' || h1 > '9'+ & \verb+h1 < '0'+ & killed \\ % ID: 2285
-    COR & 730 & \verb+h1 < '0' || h1 > '9'+ & \verb+h1 > '9'+ & killed \\ % ID: 2286
-    COR & 730 & \verb+h1 < '0' || h1 > '9'+ & \verb+true+ & killed \\ % ID: 2287
-    STD & 731 & \verb+return false;+ & \verb+<NO-OP>+ & killed \\ % ID: 2289
-    STD & 735 & \verb+return false;+ & \verb+<NO-OP>+ & live \\ % ID: 2304
-    STD & 739 & \verb+return false;+ & \verb+<NO-OP>+ & killed \\ % ID: 2319
-    LVR & 763 & \verb+false+ & \verb+true+ & killed \\ % ID: 2382
-    LVR & 766 & \verb+false+ & \verb+true+ & killed \\ % ID: 2384
-    LVR & 769 & \verb+true+ & \verb+false+ & killed % ID: 2386
-    \end{tabular}
-    \end{center}
     \end{answer}
 
     \item For each of the applied mutation operators, pick a distinct method of your project that was affected by that operator, and highlight / describe the instructions that are changed. Explain how the test suite does or does not satisfy the criteria of \textit{Reachability}, \textit{Infection}, and \textit{Propagation} for that part.
     \begin{answer}
-    \begin{center}
+    [TODO: Add answer here]
-    \begin{tabular}{l|c|c|c|c|c}
-    Function & Operator & Line & Original & Mutation & Killed \\ \hline \hline
-    \texttt{scanISO8601DateIfMatch} & EVR & 442 & \verb#c0# & \verb#0# & live \\ % ID: 1075
-    \texttt{checkTime} & COR & 730 & \verb+h1 < '0' || h1 > '9'+ & \verb+h1 < '0'+ & killed \\ % ID: 2285
-    \texttt{subString} & AOR & 161 & \verb#offset + count# & \verb#offset % count# & killed \\ % ID: 195
-    \end{tabular}
-    \end{center}
-
-    For the EVR the test suite fails does not cover the line. If \verb+c0+ was non-zero, infection would be guaranteed, but since the mutation is not reachable by the test suite it is a live mutation.
-    The COR has been killed strongly, because the line of code was reached by my extended test suite from the last exercise, and infection has been observed, because I had added a test case that has \verb+h1 > '9'+ which is not caught by the mutated code. The infection propagates directly because the condition directly branches to the return statement.
-    The AOR in the \texttt{subString} function is also killed by three of my \texttt{inputTokenTest} methods from a previous exercise and also two of Mark's tests. This method is at the core of the scanner as it is used to stringify the buffer at the current location to pass it on to specific parser methods. It is thus easily reached by the test suite and will most certainly infect any valid inputs. The propagation is also rather trivially visible as the infected method will return an incorrect string length and thus wrong buffer contents.
     \end{answer}
 
     \item Pick one suitable method (restricted to int values) or class from your project, and derive an automaton expressing its behaviour. For the creation of your automaton, use the \textit{Uppaal} model checker environment.
     \begin{answer}
-    For this exercise I selected a helper method from the \texttt{TypeUtils} class, namely the \texttt{num(char, char, char, char)} method that takes 4 digit characters and converts them to the corresponding 4 digit number. If the digits are invalid, i.e. non-digit characters, the output is $-1$.
+    [TODO: Add answer here]
     \end{answer}
 
     \item Formulate at least 2 formal requirements that your model / method needs to satisfy, create corresponding \textit{queries} in Uppaal, and execute them to assure that your base model satisfies them. Enable \texttt{Options $\rightarrow$ Diagnostic Trace $\rightarrow$ Some} to get a counterexample trace in case that a queried formula is not satisfied. This trace can be inspected in the \texttt{Simulator} tab.
     \begin{answer}
-    \begin{enumerate}
+    [TODO: Add answer here]
-      \item \texttt{A[] not deadlock || NUM.End} assures that the model will never deadlock except for the end location, meaning that the function always returns. This property is easily satisfied as there are no loops or complex behaviours in the model.
-      \item \texttt{A[] NUM.End imply (NUM.c >= -1 \&\& NUM.c < 10000)} assures that the return value of the function is always a 4 digit number or negative one. This property is also satisfied by the model.
-      \item \texttt{A[] (NUM.End imply (NUM.c1 == 48 \&\& NUM.c1 == 49 \&\& NUM.c2 == 50 \&\& NUM.c3 == 51 imply NUM.c == 1234))} is a simple test case for the assertion \texttt{num('1', '2', '3', '4') == 1234}.
-      \item \texttt{A[] (NUM.End \&\& NUM\_MUT.End) imply (NUM.c == NUM\_MUT.c)} verifies that for all executions of the function and the mutated function, i.e. when the functions each have reached their end state, have equal return values. This indicates that the mutation does not influence the function behaviour. In our example this property does not hold, because the mutation removes a boundary check. UPPAAL returns as a counterexample trace the inputs \texttt{num('9', '1', '6', ':')} for which the ground string function correctly returns $-1$ while the mutation missing the boundary check for the last character outputs $9170$.
-    \end{enumerate}
     \end{answer}
 
     \item Apply \textit{one} mutation operator from Table~\ref{table:operators} to \textit{one} single expression in your model, and re-evaluate your queries. Explain why the verification results of the model changed or remained the same. If a counterexample is created, note the test vector that kills the mutant.
     \begin{answer}
-    Here are the results for each of the properties from the previous subtask.
+    [TODO: Add answer here]
-    \begin{enumerate}
-      \item Since only one branch property changed and not the model structure the function still does not deadlock so the property still holds and cannot be killed by this property.
-      \item This property strongly killes the mutation because an edge case is now missing for the last character. The validator gives the counterexample trace input \texttt{num('9', '9', '9', ':')}, which now incorrectly outputs $10000$. The result should be $-1$ because \texttt{':'} isn't a digit character.
-      \item The last property still holds because the simple test case does not catch the mutated edge case.
-      \item This property already compares the function to its mutation so the task does not apply here.
-    \end{enumerate}
     \end{answer}
 
     \item Reroute one transition in your model (i.e., connect the edge to a different destination node), and re-evaluate your queries. Explain why the verification results of the model changed or remained the same. If a counterexample is created, note the test vector that kills the mutant.
     \begin{answer}
-    With the branch mutation (see model file), most properties still hold except for the deadlock property. This is because the properties are written as \texttt{A[] NUM.End imply ...}, but since the mutated version never reaches the end this property is always true. The deadlock property however is violated because now the model can be in a deadlock state without reaching the end state (note, that for modelling a deadlock here we require another guard to avoid a livelock situation here).
+    [TODO: Add answer here]
     \end{answer}
 
 \end{enumerate}