From c76e075ac4dce7d37f30c417a353d59db5699654 Mon Sep 17 00:00:00 2001 From: Michael Chen Date: Tue, 12 Jul 2022 20:49:28 +0200 Subject: [PATCH] Created TypeUtils.num(char[4]) uppaal model (trivial) --- .../Mutation_Testing_Sample_Model.xml | 251 +++++++----------- 1 file changed, 91 insertions(+), 160 deletions(-) diff --git a/project_task_sheets/phase_05/project_phase05_tasks/Mutation_Testing_Sample_Model.xml b/project_task_sheets/phase_05/project_phase05_tasks/Mutation_Testing_Sample_Model.xml index 4f6a02e..28e64e5 100644 --- a/project_task_sheets/phase_05/project_phase05_tasks/Mutation_Testing_Sample_Model.xml +++ b/project_task_sheets/phase_05/project_phase05_tasks/Mutation_Testing_Sample_Model.xml @@ -1,20 +1,13 @@ - // Place global declarations here. + typedef int[-2,12] digit; +broadcast chan initialized; - // As input to your method / class model, you can use either... -typedef int[-25,25] cust_t; // ... a custom integer type which is restricted to a certain value range... - -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; +int c0_in = 0; +int c1_in = 0; +int c2_in = 0; +int c3_in = 0; - - // Place template instantiations here. + NUM = Number(); +NUM_MUT = NumberMutant(); +IN_RANGE = InputFromRange(); -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 IN_RANGE, NUM, NUM_MUT; - A[] (SE.End && SE_MUT.End) imply (SE.x == SE_MUT.x && SE.y == SE_MUT.y) - - 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) - + A[] (NUM.End && NUM_MUT.End) imply (NUM.c == NUM_MUT.c) + - A[] SE.End imply (SE.x == SE.y) - - 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) - + A[] NUM.End imply (NUM.c >= -1 && NUM.c < 10000) + - A[] SE.End imply (SE.y == y_in) - - 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) - + A[] NUM_MUT.End imply (NUM_MUT.c >= -1 && NUM_MUT.c < 10000) +