TCS / Software / lpeq / Examples
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science


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 >
3: Warning: predicate 'a/0' doesn't occur in any rule head.
$ more
1 2 1 1 3
2 c
3 a

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 It is possible to add b to the symbol table by, for example, inserting a line "4 b" to the symbol table in Files, and 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 >

The composition 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 | smodels 1
$ lpeq | 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 | lpcat -m - | smodels 1
Second direction is verified in the same way.
$ lpeq -m | lpcat -m - | 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 | lpcat -m - | smodels 1
$ lpeq -m | lpcat -m - | 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 | smodels 1
smodels version 2.32. Reading...done
Answer: 1
Stable Model: a c'
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