cpsa-4.4.4: src/cpsa4prolog.pl

% -*- mode: prolog -*-

%% Library of predicates for analyzing cpsa4prolog output

%% The cpsa4prolog program is used to analyze the output of cpsa4.  It
%% translates cpsa4 output into a Prolog database that captures the
%% essential features of the output in a form that can be queried
%% using all of the power of Prolog.

%% cpsa4prolog assembles the skeletons in the output into a forest of
%% derivation trees.  It then prints the forest in Prolog syntax.  To
%% be loadable by Prolog, the output must be sorted so that clauses of
%% one predicate are colocated.  The sorting program provided in all
%% dialects of Unix does the job.

%% The output should be used by SWI Prolog as strings must not be
%% atoms.  Load the file generated by cpsa4prolog using consult/1.
%% Next load your query.  This file contains useful predicates that
%% may help formulate your query.  The comments for each predicate are
%% intended help users understand the output format.

%% Copyright (c) 2024 The MITRE Corporation

%% This program is free software: you can redistribute it and/or
%% modify it under the terms of the BSD License as published by the
%% University of California.

%% PATHS

%% The predicate path(L, Ls) is true if Ls is a path through the
%% derivation tree that starts with label L and ends with the label of
%% a skeleton that is at the root of the tree that contains L.  The
%% path predicate uses the step/3 predicate to determine if a skeletion
%% was derived from another skeleton.

%% The step predicate defines a transition relation for individual
%% cpsa4 steps.  step(P, O, L) is true if a cpsa4 step that started at
%% the skeleton labeled P produced a skeleton labeled L using the
%% operation O.  Notice that the same skeleton can appear as the
%% result of a step starting at different skeletons.  This means the
%% path predicate can find more than one path to the root.

%% For the path predicate, the operation field information is not
%% used.

path(L, [L]) :-
    root(L).

path(L, [L|Ls]) :-
    step(P, _, L),
    path(P, Ls).

%% A derivation tree is really a directed acyclic graph.  If the links
%% used for seen children are removed, the derivation tree becomes a
%% true tree--every child has exactly one parent.  The child/2
%% predicate encodes that relation.  It is used to traverse the tree
%% without revisiting a skeleton twice.  One can use it to count the
%% number of skeletons in a tree, for example.  Here we use it to find
%% the terminal skeletons without deplicates.  A terminal node is one
%% that has no successors.

terminal(L) :-
    step(L, _, _), !,
    fail.
terminal(_).

acc(W, W).
acc(W, X) :-
    child(W, Y),
    acc(Y, X).

%% A query to find the terminal skeletons using these predicates follows.

%% ask(L) :-
%%    root(W), acc(W, L), terminal(L).

%% SKELETON ASSOCIATION LISTS

%% The body of a skeleton is available as an association list.  It can
%% be queried using has_key_val(L, K, V), where L is a skeleton label,
%% K is a key, and V is its value.

has_key_val(L, K, V) :-
    skel(L, A),
    assoc(A, K, V).

assoc([[K | V] | _], K, V).
assoc([_ | A], K, V) :-
    assoc(A, K, V).

%% A query to find the labels of skeletons that are not eventually
%% dead follows.

%% ask(L) :-
%%     root(W), acc(W, L), acc(L, X), terminal(X), \+has_key_val(X, dead, _).

%% ask_all(Ls) :-
%%     findall(L, ask(L), Ls).

%% *************************************************************A

%% Goal language

%% p(K, R, S, L) is true if skeleton K has a strand S that is an
%% instance of role R as a string of length L.

%% Listener case
p(K, "", S, L) :-
    !,
    strand(K, S, [deflistener | _]),
    L == 2.
%% Non-listener case
p(K, R, S, L) :-
    atom_string(Ra, R),
    strand(K, S, [defstrand, Ra, L | _]).

%% p(K, R, V, S, T) if true if skeleton K has a strand S that is an
%% instance of role R as a string that binds role variable V as a
%% string to term T.

%% Listener case
p(K, "", S, V, T) :-
    !,
    V == "x",
    strand(K, S, [deflistener, T]).
p(K, R, V, S, T) :-
    atom_string(Ra, R),
    atom_string(Va, V),
    strand(K, S, [defstrand, Ra, _, Args]),
    assoc(Args, Va, [T]).

%% prec(K, S1, I1, S2, I2) is true if skeleton K has an ordering from
%% node (S1, I1) to node (S2, I2).
prec(K, S1, I1, S2, I2) :-
    skel(K, Alist),
    assoc(Alist, precedes, Ans),
    member([[S1, I1], [S2, I2]], Ans).

%% leads_to(K, S1, I1, S2, I2) is true if skeleton K has a leads-to
%% ordering from node (S1, I1) to node (S2, I2).
leads_to(K, S1, I1, S2, I2) :-
    skel(K, Alist),
    assoc(Alist, leads_to, Ans),
    member([[S1, I1], [S2, I2]], Ans).

%% non(K, T) is true if skeleton K has a non-originating term T.
non(K, T) :-
    skel(K, Alist),
    assoc(Alist, non_orig, Ans),
    member(T, Ans).

%% pnon(K, T) is true if skeleton K has a penetrator non-originating
%% term T.
pnon(K, T) :-
    skel(K, Alist),
    assoc(Alist, pen_non_orig, Ans),
    member(T, Ans).

%% uniq(K, T) is true if skeleton K has a uniquely originating term T.
uniq(K, T) :-
    skel(K, Alist),
    assoc(Alist, uniq_orig, Ans),
    member(T, Ans).

%% ugen(K, T) is true if skeleton K has a uniquely generating term T.
ugen(K, T) :-
    skel(K, Alist),
    assoc(Alist, uniq_gen, Ans),
    member(T, Ans).

%% fact(K, P, As) is true if skeleton K has the fact [P | As].
fact(K, P, As) :-
    skel(K, Alist),
    assoc(Alist, facts, Ans),
    member([P | As], Ans).