Skip to main content.

Param example

Model File

The model file param_example.xml can be found here. Basically a,b, and c are channels and cl is a clock. The environment (Env) can send a(1), a(2), or b. The controller (Ctl) sends c if there is an timeout in location waitc. The global variable p functioning as a parameter and should be set to NULL (not used) when it is not used.

Ctl process Env process

Printer Configuration File

We here use a configuration file param_cnf.xml, that can be found here. This file tells CoVer how to interpret the traces. Inside the coverconf tag, there is a iaprint tag, which stands for InterActionPRINTER. A sync tag tells CoVer to print an interaction (message) if the specific synchronization (channel) is used. Inside the sync tag the variable considered as parameters to the sync is given. A variable can have a type declared with the type tag. If it has the symbolic values of the tag used in the printed output.

<?xml version="1.0" ?>
<coverconf>
<iaprint>

<type name="paramtype">
   <typevalue name="NULL" value="-1" />
   <typevalue name="valueis1" value="1" />
   <typevalue name="valueis2" value="2" />
</type>

 <sync name="a" >
   <var type="paramtype">p</var>
 </sync>

 <sync name="b" >
 </sync>

 <sync name="c" >
 </sync>

 <removeval>NULL</removeval>
</iaprint>

</coverconf>

Property

As property we use param_edge.q

cover edgeObs ({Ctl}) restrict (Ctl) 

With this property we will cover all edges is the Ctl process. The observer saved in edgeObs.obs looks like this:

observer edgeObs (procid P;) {
node edgeN (edgeid) ;
rule start to edgeN(E) with E := edge (P) ;
accepting edgeN;
}
It has only one node collecting all different edges from the parameter process P (which we instantiate to Ctl in the property).

Run

Now we can create the trace.

./CoVer.exe -t 0 -G -K param_cnf.xml -f param.tr param_example.xml param_edge.q

The trace is directed to the file param.tr which looks like this:

<?xml version="1.0" ?>
<!-- Generated by Uppaal CoVer -->
<traces>
<trace>
<sync name="a">
    <var name="p">valueis1</var>
</sync>
<sync name="b">
</sync>
</trace>
<trace>
<sync name="a">
    <var name="p">valueis1</var>
</sync>
<delay>3</delay>
<sync name="c">
</sync>
</trace>
<trace>
<sync name="a">
    <var name="p">valueis2</var>
</sync>
<sync name="b">
</sync>
</trace>
<traces>
The test suite has three traces. In the first trace we have "a(1), b". In the second "a(1), delay 3, c", and in the third "a(2), b".

Also printed is some "meta" information about the test suite. In this case we have one parameter for the edgeN node in the observer, that is of type edgeid. The edges are named with the pattern <source_loc>_to_<target_loc>. The unnamed committed location has been named "_id6" by UPPAAL. (Observe that the Traces and TotCost values are bogus...)

CovItems=6
Traces=0
TotCost=0
TotLength=15
 edgeN<edgeid Ctl.waita_to__id6>  edgeN<edgeid Ctl._id6_to_waitc>
 edgeN<edgeid Ctl._id6_to_waitb>  edgeN<edgeid Ctl.waitc_to_waitb>
 edgeN<edgeid Ctl.waitc_to_waita>  edgeN<edgeid Ctl.waitb_to_waitc>