plai_db (answer table) comparator

Author(s): Isabel Garcia-Contreras.

This module compares instances of plai databases that are present in plai_db_instances, independently of their representation.

After computing two plai dbs (DB1 and DB2) with compare(DB1, DB2, AbsInt, Diff), several types of differences may appear in a list of elements abs_diff(Id2, AbsInt, DBId2, Sg:Call, Succ, new)

* modif(Sg:Call, Succ, Succ2) : means that there is a tuple in both dbs but the success pattern is not the same in both. It is Succ in DB1 and Succ2 in DB2.

* contained(Sg:Call) : means that the call pattern in DB1 Sg:Call is not in DB1 but it is contained in one more general in DB2

* not_in(Sg:Call) : means there is a tuple for Sg:Call in DB1 but there is not in DB2.

* new : means that the tuple of DB2 does not exist in DB1.

Module Incremental modular analysis sequence checker is an example of use of this module.


Usage and interface

Documentation on exports

PREDICATEcompare/4

Usage:compare(DBId1,DBId2,AbsInt,Diff)

Compares two previously loaded abstract databases of domain AbsInt, DBId1 and DBId2 to produce a list with the differences in Diff, expressed relative to database DBId1.

  • The following properties should hold at call time:
    (atm/1)DBId1 is an atom.
    (atm/1)DBId2 is an atom.
    (atm/1)AbsInt is an atom.
    (var/1)Diff is a free variable.
  • The following properties should hold upon exit:
    (list/2)Diff is a list of abs_diff_types.

Usage:check_same_success(AbsInt,Succ1,Succ2)

Succeeds if Succ1 and Succ2 are quivalent abstract substitution patterns.

  • The following properties should hold at call time:
    (atm/1)AbsInt is an atom.

Usage:check_same_calls(AbsInt,Sg1,Call1,Sg2,Call2)

Succeeds if Call1 and Call2 are quivalent call patterns for goals Sg1 and Sg2.

  • The following properties should hold at call time:
    (atm/1)AbsInt is an atom.

Documentation on imports

This module has the following direct dependencies: