Examples
Verification of visible equivalence
To appear.
Verification of strong equivalence
To appear.
Verification of weak equivalence for disjunctive programs
To appear
Verification of modular equivalence
Consider programs P and Q consisting of modules
P1, P2, Q1, Q2. The encodings of the
modules in the input language of lparse are as follows:
 p1.lp: 
#external a,b. 
 p2.lp: 
#external b. 
  c : not a. 
  a : b. 

q1.lp:  #external a,b. 
 q2.lp: 
#external a. 
  c : not b. 
  b : a. 
Declaration #external is used to tell lparse
which atoms are not defined inside the module. This declaration
does not match exactly what we would like the declaration of input
atoms to be, but currently there is no direct support for declaring
input atoms in lparse .
Information hiding, however, can be obtained using
#hide declaration. For more details see the
user's manual of lparse .
lparse can be used to obtain the presentation of the
modules in the internal format of smodels which is also
the input format for lpeq and lpcat . For
example, in the case of module P1:
$ lparse p1.lp > p1.sm
3: Warning: predicate 'a/0' doesn't occur in any rule
head.
$ more p1.sm
1 2 1 1 3
0
2 c
3 a
0
B+
0
B
1
0
1
Since lparse is designed for programs with a completely
specified input, there is a warning message. Notice also that
since atom b does not occur in the rules of P1
it does not appear in the symbol table of p1.sm .
It is possible to add b to the symbol table by, for
example, inserting a line "4 b " to the symbol table in
p1.sm .
Files p2.sm , q1.sm and q2.sm
can be obtained similarly from files
p2.lp , q1.lp and q2.lp ,
respectively.
lpcat computes the join of two modules with flag
m . For example, the composition P1 ⊕ P2
is obtained as follows.
$ lpcat m p1.sm p2.sm > p1p2.sm
The composition q2p2.sm can be obtained similarly.
Now, we are ready to use lpeq to verify the equivalence
of P and Q.
First, we can verify the equivalence without taking into account our
knowledge about the modular structure using the following commands.
$ lpeq p1p2.sm q1q2.sm  smodels 1
$ lpeq q1q2.sm p1p2.sm  smodels 1
The modular approach to equivalence verification goes as follows.
In the first step one computes the translation
EQT(P1,Q1) using lpeq with flag m .
The context module P2 is added using the tool
lpcat with flag m and smodels
is used to see if the translation
EQT(P1,Q1)⊕ P2 has stable models.
$ lpeq m p1.sm q1.sm  lpcat m  p2.sm  smodels 1
Second direction is verified in the same way.
$ lpeq m q1.sm p1.sm  lpcat m  p2.sm  smodels 1
Since neither translation has stable models we learn that
P1 ⊕ P2 is modularly equivalent to
Q1 ⊕ P2.
The second equivalence in the chain, that is,
the equivalence of Q1 ⊕ P2 and
Q1 ⊕ Q2, is verified similarly:
$ lpeq m p2.sm q2.sm  lpcat m  q1.sm  smodels 1
$ lpeq m q2.sm p2.sm  lpcat m  q1.sm  smodels 1
It is also possible to use a different order in the chaining of
modules.
Even though modules P1 and Q1
behave equivalently in the contexts of P2 and Q2, they
are not modularly equivalent in general.
This can be verified using the translation without a specific context.
Note that the translation EQT(P1,Q1) is a
module with input {a,b} . To be able to compute its stable
models using the current smodels one needs to attach an
input generator.
This can be obtained automatically using flag i in
lpeq .
$ lpeq m i p1.sm q1.sm  smodels 1
smodels version 2.32. Reading...done
Answer: 1
Stable Model: a c'
True
Duration: 0.002
Number of choice points: 1
Number of wrong choices: 0
Number of atoms: 9
Number of rules: 8
Number of picked atoms: 3
Number of forced atoms: 0
Number of truth assignments: 13
Size of searchspace (removed): 2 (2)
The stable model {a,c'} for translation
EQT(P1,Q1) gives us a counterexample for the modular
equivalence of P1 and Q1:
{a} is a stable model of P1
and {a,c} is the least model of Q1 with respect to
the input {a} .
[TCS main]
[Contact Info]
[Personnel]
[Research]
[Publications]
[Software]
[Studies]
[News Archive]
[Links]
Latest update: 06 February 2013.
Emilia Oikarinen
