Putting all together:

Model File

A simple model file to show definition-use coverage. This file is saved as dusys.xml

Property

We save

cover duVar ({x}) restrict (ctl)

To the file PropDU.q

Observer

We save

observer duVar (varid X;) {
 node defined (varid, edgeid);
 node du (varid, edgeid, edgeid);

 rule start        to defined(X,E) with def(X,E);
 rule defined(X,E) to defined(X,E) with no def(X);
 rule defined(X,E) to du(X,E,E2)   with use(X,E2);

 accepting du;
}

To the file duVar.obs

Run

Now we can create the trace.

./CoVer.exe -t 0 -G -f duTraces.tr  dusys.xml PropDU.q 

In file duTraces.tr we find

===== Trace #1===================================
 du<varid offset=0, edgeid ctl.id1_to_id2, edgeid ctl.id2_to_id3> 
State:
( ctl.id1 )
x=0 
mincost: 0

Transitions:
  ctl.id1->ctl.id2 { 1, tau, x := 1 }

State:
( ctl.id2 )
x=1 
mincost: 0

Transitions:
  ctl.id2->ctl.id3 { 1, tau, x := x + 1 }

State:
( ctl.id3 )
x=2 
mincost: 0

===== Trace #2===================================
 du<varid offset=0, edgeid ctl.id1_to_id2, edgeid ctl.id2_to_id4> 
State:
( ctl.id1 )
x=0 
mincost: 0

Transitions:
  ctl.id1->ctl.id2 { 1, tau, x := 1 }

State:
( ctl.id2 )
x=1 
mincost: 0

Transitions:
  ctl.id2->ctl.id4 { 1, tau, x := x + 2 }

State:
( ctl.id4 )
x=3 
mincost: 0