Created TypeUtils.num(char[4]) uppaal model (trivial)
This commit is contained in:
parent
ba3078b2b5
commit
c76e075ac4
@ -1,20 +1,13 @@
|
||||
<?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>// Place global declarations here.
|
||||
<declaration>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;</declaration>
|
||||
int c0_in = 0;
|
||||
int c1_in = 0;
|
||||
int c2_in = 0;
|
||||
int c3_in = 0;</declaration>
|
||||
<template>
|
||||
<name>InputFromRange</name>
|
||||
<location id="id0" x="-238" y="-204">
|
||||
@ -34,195 +27,133 @@ int y_in = 0;</declaration>
|
||||
<transition>
|
||||
<source ref="id1"/>
|
||||
<target ref="id2"/>
|
||||
<label kind="select" x="-637" y="-238">xi : cust_t, yi : cust_t</label>
|
||||
<label kind="assignment" x="-620" y="-187">x_in = xi, y_in = yi</label>
|
||||
<label kind="select" x="-603" y="-297">c0_val : digit,
|
||||
c1_val : digit,
|
||||
c2_val : digit,
|
||||
c3_val : digit</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>InputFromList</name>
|
||||
<location id="id3" x="42" y="8">
|
||||
<urgent/>
|
||||
<name x="5" y="5">Number</name>
|
||||
<declaration>int c0 = 0;
|
||||
int c1 = 0;
|
||||
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="238" y="9">
|
||||
<location id="id4" x="51" y="-34">
|
||||
</location>
|
||||
<location id="id5" x="-195" y="8">
|
||||
<location id="id5" x="-161" y="-33">
|
||||
<name x="-171" y="-67">Init</name>
|
||||
<urgent/>
|
||||
</location>
|
||||
<init ref="id5"/>
|
||||
<transition>
|
||||
<source ref="id3"/>
|
||||
<target ref="id4"/>
|
||||
<label kind="synchronisation" x="94" y="-16">initialized!</label>
|
||||
<source ref="id4"/>
|
||||
<target ref="id3"/>
|
||||
<label kind="guard" x="102" y="-17">!(c0 >= 0 && c0 <= 9
|
||||
&& c1 >= 0 && c1 <= 9
|
||||
&& c2 >= 0 && c2 <= 9
|
||||
&& c3 >= 0 && c3 <= 9)</label>
|
||||
<label kind="assignment" x="153" y="-68">c = -1</label>
|
||||
</transition>
|
||||
<transition>
|
||||
<source ref="id4"/>
|
||||
<target ref="id3"/>
|
||||
<label kind="guard" x="-8" y="-229">c0 >= 0 && c0 <= 9
|
||||
&& c1 >= 0 && c1 <= 9
|
||||
&& c2 >= 0 && c2 <= 9
|
||||
&& c3 >= 0 && c3 <= 9</label>
|
||||
<label kind="assignment" x="229" y="-229">c = c0 * 1000
|
||||
+ c1 * 100
|
||||
+ c2 * 10
|
||||
+ c3</label>
|
||||
<nail x="178" y="-170"/>
|
||||
</transition>
|
||||
<transition>
|
||||
<source ref="id5"/>
|
||||
<target ref="id3"/>
|
||||
<label kind="select" x="-178" y="-25">ind_x : index_t, ind_y : index_t</label>
|
||||
<label kind="assignment" x="-204" y="26">x_in = values[ind_x], y_in = values[ind_y]</label>
|
||||
<target ref="id4"/>
|
||||
<label kind="synchronisation" x="-102" y="-59">initialized?</label>
|
||||
<label kind="assignment" x="-102" y="-17">c0 = c0_in,
|
||||
c1 = c1_in,
|
||||
c2 = c2_in,
|
||||
c3 = c3_in</label>
|
||||
</transition>
|
||||
</template>
|
||||
<template>
|
||||
<name x="5" y="5">SetEqual</name>
|
||||
<declaration>// Place local declarations here.
|
||||
int x = 0;
|
||||
int y = 0;</declaration>
|
||||
<name x="5" y="5">NumberMutant</name>
|
||||
<declaration>int c0 = 0;
|
||||
int c1 = 0;
|
||||
int c2 = 0;
|
||||
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="178" y="25">
|
||||
<name x="168" y="-9">B</name>
|
||||
<location id="id7" x="51" y="-34">
|
||||
</location>
|
||||
<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">
|
||||
<location id="id8" x="-161" y="-33">
|
||||
<name x="-171" y="-67">Init</name>
|
||||
<urgent/>
|
||||
</location>
|
||||
<init ref="id10"/>
|
||||
<init ref="id8"/>
|
||||
<transition>
|
||||
<source ref="id7"/>
|
||||
<target ref="id6"/>
|
||||
<label kind="guard" x="221" y="8">!(x<y)</label>
|
||||
<label kind="guard" x="102" y="-17">!(c0 >= 0 && c0 <= 9
|
||||
&& c1 >= 0 && c1 <= 9
|
||||
&& c2 >= 0 && c2 <= 9
|
||||
&& c3 >= 0 && true)</label>
|
||||
<label kind="assignment" x="153" y="-68">c = -1</label>
|
||||
</transition>
|
||||
<transition>
|
||||
<source ref="id7"/>
|
||||
<target ref="id7"/>
|
||||
<label kind="guard" x="161" y="68">x<y</label>
|
||||
<label kind="assignment" x="161" y="102">x=x+1</label>
|
||||
<nail x="238" y="93"/>
|
||||
<nail x="102" y="93"/>
|
||||
</transition>
|
||||
<transition>
|
||||
<source ref="id8"/>
|
||||
<target ref="id8"/>
|
||||
<label kind="guard" x="161" y="-204">x>y</label>
|
||||
<label kind="assignment" x="153" y="-170">x=x-1</label>
|
||||
<nail x="246" y="-178"/>
|
||||
<nail x="93" y="-178"/>
|
||||
</transition>
|
||||
<transition>
|
||||
<source ref="id8"/>
|
||||
<target ref="id6"/>
|
||||
<label kind="guard" x="221" y="-93">!(x>y)</label>
|
||||
<label kind="guard" x="-8" y="-229">c0 >= 0 && c0 <= 9
|
||||
&& c1 >= 0 && c1 <= 9
|
||||
&& c2 >= 0 && c2 <= 9
|
||||
&& c3 >= 0 && true</label>
|
||||
<label kind="assignment" x="229" y="-229">c = c0 * 1000
|
||||
+ c1 * 100
|
||||
+ c2 * 10
|
||||
+ c3</label>
|
||||
<nail x="178" y="-170"/>
|
||||
</transition>
|
||||
<transition>
|
||||
<source ref="id9"/>
|
||||
<source ref="id8"/>
|
||||
<target ref="id7"/>
|
||||
<label kind="guard" x="76" y="0">x<y</label>
|
||||
</transition>
|
||||
<transition>
|
||||
<source ref="id9"/>
|
||||
<target ref="id8"/>
|
||||
<label kind="guard" x="76" y="-93">x>=y</label>
|
||||
</transition>
|
||||
<transition>
|
||||
<source ref="id10"/>
|
||||
<target ref="id9"/>
|
||||
<label kind="synchronisation" x="-102" y="-59">initialized?</label>
|
||||
<label kind="assignment" x="-119" y="-25">x = x_in, y = y_in</label>
|
||||
<label kind="assignment" x="-102" y="-17">c0 = c0_in,
|
||||
c1 = c1_in,
|
||||
c2 = c2_in,
|
||||
c3 = c3_in</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="id14"/>
|
||||
<target ref="id12"/>
|
||||
<label kind="guard" x="119" y="-34">x>=y</label>
|
||||
</transition>
|
||||
<transition>
|
||||
<source ref="id11"/>
|
||||
<target ref="id12"/>
|
||||
<label kind="guard" x="187" y="34">!(x<y)</label>
|
||||
</transition>
|
||||
<transition>
|
||||
<source ref="id11"/>
|
||||
<target ref="id11"/>
|
||||
<label kind="guard" x="127" y="94">x<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>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>y)</label>
|
||||
</transition>
|
||||
<transition>
|
||||
<source ref="id14"/>
|
||||
<target ref="id11"/>
|
||||
<label kind="guard" x="42" y="26">x<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>// Place template instantiations here.
|
||||
<system>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>
|
||||
system IN_RANGE, NUM, NUM_MUT;</system>
|
||||
<queries>
|
||||
<query>
|
||||
<formula>A[] (SE.End && SE_MUT.End) imply (SE.x == SE_MUT.x && SE.y == SE_MUT.y)
|
||||
</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>
|
||||
<formula>A[] (NUM.End && NUM_MUT.End) imply (NUM.c == NUM_MUT.c)</formula>
|
||||
<comment></comment>
|
||||
</query>
|
||||
<query>
|
||||
<formula>A[] SE.End imply (SE.x == SE.y)
|
||||
</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>
|
||||
<formula>A[] NUM.End imply (NUM.c >= -1 && NUM.c < 10000)</formula>
|
||||
<comment></comment>
|
||||
</query>
|
||||
<query>
|
||||
<formula>A[] SE.End imply (SE.y == y_in)
|
||||
</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>
|
||||
<formula>A[] NUM_MUT.End imply (NUM_MUT.c >= -1 && NUM_MUT.c < 10000)</formula>
|
||||
<comment></comment>
|
||||
</query>
|
||||
</queries>
|
||||
</nta>
|
||||
|
||||
Loading…
Reference in New Issue
Block a user