Added remediation computation
Incomplete but sound. Handles simple cases. All tests pass Issue: # Change-Id: Ib50ac5f28de6b10202821583309b02e3489a6e65
This commit is contained in:
Tim Hinrichs
parent
ad9941d0b0
commit
ef84b421b5
|
|
@ -0,0 +1,18 @@
|
|||
|
||||
|
||||
// disconnect_network action
|
||||
action(disconnect_network)
|
||||
nova:network-(vm, network) :- disconnect_network(vm, network)
|
||||
|
||||
// delete_vm action
|
||||
action(delete_vm)
|
||||
nova:virtual_machine-(vm) :- delete_vm(vm)
|
||||
nova:network-(vm, network) :- delete_vm(vm), nova:network(vm, network)
|
||||
nova:owner-(vm, owner) :- delete_vm(vm), nova:owner(vm, owner)
|
||||
|
||||
// make_public action
|
||||
action(make_public)
|
||||
neutron:public_network+(network) :- make_public(network)
|
||||
|
||||
|
||||
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
A script for a demo.
|
||||
. script for a demo.
|
||||
|
||||
0) Example policy
|
||||
|
||||
|
|
@ -30,7 +30,7 @@ cd congress/src/policy
|
|||
python
|
||||
>>> import runtime
|
||||
>>> r = runtime.Runtime()
|
||||
>>> r.load_file("../../examples/private_public_network")
|
||||
>>> r.load_file("../../examples/private_public_network.classify")
|
||||
-------------------------------------------------
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -92,7 +92,11 @@ variable
|
|||
;
|
||||
|
||||
relation_constant
|
||||
: ID (':' ID)* -> ^(STRUCTURED_NAME ID+)
|
||||
: ID (':' ID)* SIGN? -> ^(STRUCTURED_NAME ID+ SIGN?)
|
||||
;
|
||||
|
||||
SIGN
|
||||
: '+' | '-'
|
||||
;
|
||||
|
||||
ID : ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'0'..'9'|'_')*
|
||||
|
|
|
|||
|
|
@ -211,7 +211,7 @@ class Atom (object):
|
|||
|
||||
def plug(self, binding, caller=None):
|
||||
"Assumes domain of BINDING is Terms"
|
||||
logging.debug("Atom.plug({}, {})".format(str(binding), str(caller)))
|
||||
# logging.debug("Atom.plug({}, {})".format(str(binding), str(caller)))
|
||||
new = copy.copy(self)
|
||||
if isinstance(binding, dict):
|
||||
args = []
|
||||
|
|
@ -231,6 +231,10 @@ class Atom (object):
|
|||
def argument_names(self):
|
||||
return tuple([arg.name for arg in self.arguments])
|
||||
|
||||
def make_positive(self):
|
||||
""" Does NOT make copy """
|
||||
return self
|
||||
|
||||
|
||||
class Literal(Atom):
|
||||
""" Represents either a negated atom or an atom. """
|
||||
|
|
@ -275,6 +279,12 @@ class Literal(Atom):
|
|||
new.negated = not new.negated
|
||||
return new
|
||||
|
||||
def make_positive(self):
|
||||
""" Copies SELF and makes is_negated False. """
|
||||
new = copy.copy(self)
|
||||
new.negated = False
|
||||
return new
|
||||
|
||||
class Rule (object):
|
||||
""" Represents a rule, e.g. p(x) :- q(x). """
|
||||
def __init__(self, head, body, location=None):
|
||||
|
|
@ -563,7 +573,11 @@ class CongressSyntax (object):
|
|||
@classmethod
|
||||
def create_structured_name(cls, antlr):
|
||||
# (STRUCTURED_NAME (ARG1 ... ARGN))
|
||||
return ":".join([x.getText() for x in antlr.children])
|
||||
if antlr.children[-1].getText() in ['+', '-']:
|
||||
return (":".join([x.getText() for x in antlr.children[:-1]]) +
|
||||
antlr.children[-1].getText())
|
||||
else:
|
||||
return ":".join([x.getText() for x in antlr.children])
|
||||
|
||||
@classmethod
|
||||
def create_term(cls, antlr):
|
||||
|
|
@ -605,15 +619,18 @@ def print_tree(tree, text, kids, ind=0):
|
|||
## Mains
|
||||
##############################################################################
|
||||
|
||||
def get_compiled(args):
|
||||
""" Run compiler as per ARGS and return the resulting Compiler instance. """
|
||||
compiler = get_compiler(args)
|
||||
compiler.compute_delta_rules()
|
||||
return compiler
|
||||
def parse(policy_string):
|
||||
""" Run compiler on policy string and return the parsed formulas. """
|
||||
compiler = get_compiler([policy_string, '--input_string'])
|
||||
return compiler.theory
|
||||
|
||||
def get_parsed(args):
|
||||
""" Run compiler as per ARGS and return the parsed rules. """
|
||||
compiler = get_compiler(args)
|
||||
def parse1(policy_string):
|
||||
""" Run compiler on policy string and return 1st parsed formula. """
|
||||
return parse(policy_string)[0]
|
||||
|
||||
def parse_file(filename):
|
||||
""" Run compiler on policy stored in FILENAME and return the parsed formulas. """
|
||||
compiler = get_compiler([filename])
|
||||
return compiler.theory
|
||||
|
||||
def get_compiler(args):
|
||||
|
|
|
|||
|
|
@ -90,6 +90,14 @@ class Proof(object):
|
|||
s += child.str_tree(depth + 1)
|
||||
return s
|
||||
|
||||
def leaves(self):
|
||||
if len(self.children) == 0:
|
||||
return [self.root]
|
||||
result = []
|
||||
for child in self.children:
|
||||
result.extend(child.leaves())
|
||||
return result
|
||||
|
||||
class DeltaRule(object):
|
||||
def __init__(self, trigger, head, body, original):
|
||||
self.trigger = trigger # atom
|
||||
|
|
@ -145,7 +153,6 @@ class TopDownTheory(object):
|
|||
def __init__(self, binding, support):
|
||||
self.binding = binding
|
||||
self.support = support # for abduction
|
||||
logging.debug(str(self))
|
||||
|
||||
def __str__(self):
|
||||
return "TopDownResult(binding={}, support={})".format(
|
||||
|
|
@ -205,6 +212,18 @@ class TopDownTheory(object):
|
|||
return [query.plug(x) for x in bindings]
|
||||
|
||||
def explain(self, query, tablenames, find_all=True):
|
||||
""" Same as select except stores instances of TABLENAMES
|
||||
that participated in each proof. If QUERY is an atom,
|
||||
returns list of rules with QUERY in the head and
|
||||
the stored instances of TABLENAMES in the body; if QUERY is
|
||||
a rule, the rules returned have QUERY's head in the head
|
||||
and the stored instances of TABLENAMES in the body. """
|
||||
# This is different than abduction because instead of replacing
|
||||
# a proof attempt with saving a literal, we want to save a literal
|
||||
# after a successful proof attempt.
|
||||
assert False, "Not yet implemented"
|
||||
|
||||
def abduce(self, query, tablenames, find_all=True):
|
||||
""" Computes additional literals that if true would make
|
||||
(some instance of) QUERY true. Returns a list of rules
|
||||
where the head represents an instance of the QUERY and
|
||||
|
|
@ -215,8 +234,8 @@ class TopDownTheory(object):
|
|||
(and hence the head) true. If FIND_ALL is true, the
|
||||
return list has at most one element.
|
||||
Limitation: every negative literal relevant to a proof of
|
||||
QUERY is true, i.e. no literals are saved when proving a negative
|
||||
literal is true."""
|
||||
QUERY is unconditionally true, i.e. no literals are saved
|
||||
when proving a negative literal is true."""
|
||||
assert (isinstance(query, compile.Atom) or
|
||||
isinstance(query, compile.Rule)), \
|
||||
"Explain requires a formula"
|
||||
|
|
@ -232,7 +251,7 @@ class TopDownTheory(object):
|
|||
find_all=find_all, save=lambda lit,binding: lit.table in tablenames)
|
||||
results = [compile.Rule(output.plug(abd.binding), abd.support)
|
||||
for abd in abductions]
|
||||
logging.debug("MRT's explain result: " + iterstr(results))
|
||||
logging.debug("abduction result: " + iterstr(results))
|
||||
return results
|
||||
|
||||
def top_down_evaluation(self, variables, literals,
|
||||
|
|
@ -247,10 +266,10 @@ class TopDownTheory(object):
|
|||
# str(binding)))
|
||||
results = self.top_down_abduction(variables, literals,
|
||||
binding=binding, find_all=find_all, save=None)
|
||||
logging.debug("EXIT: top_down_evaluation(vars={}, literals={}, "
|
||||
"binding={}) returned {}".format(
|
||||
iterstr(variables), iterstr(literals),
|
||||
str(binding), iterstr(results)))
|
||||
# logging.debug("EXIT: top_down_evaluation(vars={}, literals={}, "
|
||||
# "binding={}) returned {}".format(
|
||||
# iterstr(variables), iterstr(literals),
|
||||
# str(binding), iterstr(results)))
|
||||
return [x.binding for x in results]
|
||||
|
||||
def top_down_abduction(self, variables, literals, binding=None,
|
||||
|
|
@ -676,83 +695,6 @@ class Database(TopDownTheory):
|
|||
""" THING1 is always a ground DBTuple and THING2 is always an ATOM. """
|
||||
return dbtuple.match(atom, unifier2)
|
||||
|
||||
|
||||
# Old version of database-specific top_down_eval
|
||||
# def top_down_eval(self, context, caller):
|
||||
# """ Implementation of top_down_eval required to include
|
||||
# Database within RuleTheory. """
|
||||
# bindings = self.top_down_eval_aux(context.literals,
|
||||
# context.literal_index, context.binding)
|
||||
|
||||
# def top_down_eval_aux(self, literals, literal_index, binding):
|
||||
# """ Compute all instances of LITERALS (from LITERAL_INDEX and above) that
|
||||
# are true in the Database (after applying the dictionary binding
|
||||
# BINDING to LITERALS). Returns a list of dictionary bindings. """
|
||||
# if literal_index > len(literals) - 1:
|
||||
# return [binding]
|
||||
# lit = literals[literal_index]
|
||||
# self.log(lit.table, ("Top_down_eval(literals={}, literal_index={}, "
|
||||
# "bindings={})").format(
|
||||
# "[" + ",".join(str(x) for x in literals) + "]",
|
||||
# literal_index,
|
||||
# str(binding)),
|
||||
# depth=literal_index)
|
||||
# # assume that for negative literals, all vars are bound at this point
|
||||
# # if there is a match, data_bindings will contain at least one binding
|
||||
# # (possibly including the empty binding)
|
||||
# data_bindings = self.matches(lit, binding)
|
||||
# self.log(lit.table, "data_bindings: " + str(data_bindings), depth=literal_index)
|
||||
# # if not negated, empty data_bindings means failure
|
||||
# if len(data_bindings) == 0 :
|
||||
# return []
|
||||
|
||||
# results = []
|
||||
# for data_binding in data_bindings:
|
||||
# # add new binding to current binding
|
||||
# binding.update(data_binding)
|
||||
# if literal_index == len(literals) - 1: # last element
|
||||
# results.append(dict(binding)) # need to copy
|
||||
# else:
|
||||
# results.extend(self.top_down_eval_aux(literals,
|
||||
# literal_index + 1, binding))
|
||||
# # remove new binding from current bindings
|
||||
# for var in data_binding:
|
||||
# del binding[var]
|
||||
# self.log(lit.table, "Top_down_eval return value: {}".format(
|
||||
# '[' + ", ".join([str(x) for x in results]) + ']'), depth=literal_index)
|
||||
|
||||
# return results
|
||||
|
||||
# def matches(self, literal, binding):
|
||||
# """ Returns a list of binding lists for the variables in LITERAL
|
||||
# not bound in BINDING. If LITERAL is negative, returns
|
||||
# either [] meaning the lookup failed or [{}] meaning the lookup
|
||||
# succeeded; otherwise, returns one binding list for each tuple in
|
||||
# the database matching LITERAL under BINDING. """
|
||||
# # slow for negation--should stop at first match, not find all of them
|
||||
# matches = self.matches_atom(literal, binding)
|
||||
# if literal.is_negated():
|
||||
# if len(matches) > 0:
|
||||
# return []
|
||||
# else:
|
||||
# return [{}]
|
||||
# else:
|
||||
# return matches
|
||||
|
||||
# def matches_atom(self, atom, binding):
|
||||
# """ Returns a list of binding lists for the variables in ATOM
|
||||
# not bound in BINDING: one binding list for each tuple in
|
||||
# the database matching ATOM under BINDING. """
|
||||
# if atom.table not in self.data:
|
||||
# return []
|
||||
# result = []
|
||||
# for tuple in self.data[atom.table]:
|
||||
# logging.debug("Matching database tuple {}".format(str(tuple)))
|
||||
# new_binding = tuple.match(atom, binding)
|
||||
# if new_binding is not None:
|
||||
# result.append(new_binding)
|
||||
# return result
|
||||
|
||||
def atom_to_internal(self, atom, proofs=None):
|
||||
return atom.table, self.DBTuple(atom.argument_names(), proofs)
|
||||
|
||||
|
|
@ -1078,35 +1020,6 @@ class MaterializedRuleTheory(TopDownTheory):
|
|||
self.process_new_bindings(bindings, delta_rule.head,
|
||||
insert_delete, delta_rule.original)
|
||||
|
||||
def is_view(self, x):
|
||||
return self.delta_rules.is_view(x)
|
||||
|
||||
# def process_new_bindings(self, bindings, atom, insert, original_rule):
|
||||
# """ For each of BINDINGS, apply to ATOM, and enqueue it as an insert if
|
||||
# INSERT is True and as a delete otherwise. """
|
||||
# # for each binding, compute generated tuple and group bindings
|
||||
# # by the tuple they generated
|
||||
# new_tuples = {}
|
||||
# for binding in bindings:
|
||||
# new_tuple = tuple(atom.plug(binding).to_tuple())
|
||||
# if new_tuple not in new_tuples:
|
||||
# new_tuples[new_tuple] = []
|
||||
# new_tuples[new_tuple].append(Database.Proof(
|
||||
# binding, original_rule))
|
||||
# self.log(atom.table, "new tuples generated: {}".format(
|
||||
# ", ".join([str(x) for x in new_tuples])))
|
||||
|
||||
# # enqueue each distinct generated tuple, recording appropriate bindings
|
||||
# for new_tuple in new_tuples:
|
||||
# # self.log(event.table,
|
||||
# # "new_tuple {}: {}".format(str(new_tuple), str(new_tuples[new_tuple])))
|
||||
# # Only enqueue if new data.
|
||||
# # Putting the check here is necessary to support recursion.
|
||||
# self.queue.enqueue(Event(table=atom.table,
|
||||
# tuple=new_tuple,
|
||||
# proofs=new_tuples[new_tuple],
|
||||
# insert=insert))
|
||||
|
||||
def process_new_bindings(self, bindings, atom, insert, original_rule):
|
||||
""" For each of BINDINGS, apply to ATOM, and enqueue it as an insert if
|
||||
INSERT is True and as a delete otherwise. """
|
||||
|
|
@ -1132,6 +1045,13 @@ class MaterializedRuleTheory(TopDownTheory):
|
|||
proofs=new_atoms[new_atom],
|
||||
insert=insert))
|
||||
|
||||
def is_view(self, x):
|
||||
return self.delta_rules.is_view(x)
|
||||
|
||||
def base_tables(self):
|
||||
return [table for table in self.database.table_names()
|
||||
if not self.is_view(table)]
|
||||
|
||||
def top_down_eval(self, context, caller):
|
||||
return self.database.top_down_eval(context, caller)
|
||||
|
||||
|
|
@ -1153,30 +1073,45 @@ class Runtime (object):
|
|||
self.tracer = Tracer()
|
||||
# collection of theories
|
||||
self.theory = {}
|
||||
# CLASSIFY_THEORY: the policy
|
||||
# Allow negation for sure. Currently supports recursion.
|
||||
self.theory[self.CLASSIFY_THEORY] = MaterializedRuleTheory()
|
||||
self.theory[self.SERVICE_THEORY] = NonrecursiveRuleTheory()
|
||||
# ACTION_THEORY: describes how actions affect tables
|
||||
# non-recursive, with semi-positive negation over base tables
|
||||
# of CLASSIFY_THEORY, i.e. no negation over views of
|
||||
# either ACTION_THEORY or CLASSIFY_THEORY.
|
||||
# (Why?: Using top-down eval, hence no recursion, and abduction
|
||||
# saves no literal under a negated literal.)
|
||||
# The +/- atoms (a) should only appear in the head and (b)
|
||||
# should only be for the basetables of CLASSIFY_THEORY, i.e.
|
||||
# no action should change a table that exists only in the policy.
|
||||
# Can reference tables defined in CLASSIFY_THEORY in the body
|
||||
# of rules or any other tables defined in ACTION_THEORY.
|
||||
# Should throw warning if referencing table not appearing
|
||||
# in either and provide special table False.
|
||||
self.theory[self.ACTION_THEORY] = NonrecursiveRuleTheory()
|
||||
# Service/Action theories build upon Classify theory
|
||||
self.theory[self.SERVICE_THEORY].includes.append(
|
||||
self.theory[self.CLASSIFY_THEORY])
|
||||
self.theory[self.ACTION_THEORY].includes.append(
|
||||
self.theory[self.CLASSIFY_THEORY])
|
||||
# SERVICE_THEORY: describes bindings for tables to real-world
|
||||
# software.
|
||||
# Need bindings for every base-table in CLASSIFY_THEORY
|
||||
# and every action in ACTION_THEORY.
|
||||
self.theory[self.SERVICE_THEORY] = NonrecursiveRuleTheory()
|
||||
|
||||
def log(self, table, msg, depth=0):
|
||||
self.tracer.log(table, "RT: " + msg, depth)
|
||||
|
||||
############### External interface ###############
|
||||
def get_target(self, name):
|
||||
if name is None:
|
||||
name = self.CLASSIFY_THEORY
|
||||
assert name in self.theory, "Unknown target {}".format(name)
|
||||
return self.theory[name]
|
||||
|
||||
def log(self, table, msg, depth=0):
|
||||
self.tracer.log(table, "RT: " + msg, depth)
|
||||
|
||||
############### External interface ###############
|
||||
def load_file(self, filename, target=None):
|
||||
""" Compile the given FILENAME and insert each of the statements
|
||||
into the runtime. """
|
||||
compiler = compile.get_parsed([filename])
|
||||
for formula in compiler.theory:
|
||||
for formula in compile.parse_file(filename):
|
||||
self.insert(formula, target=target)
|
||||
|
||||
def select(self, query, target=None):
|
||||
|
|
@ -1189,16 +1124,6 @@ class Runtime (object):
|
|||
else:
|
||||
return self.select_obj(query, self.get_target(target))
|
||||
|
||||
# Maybe implement one day
|
||||
# def select_if(self, query, temporary_data):
|
||||
# """ Event handler for hypothetical queries. Returns the set of
|
||||
# all instantiated QUERYs that would be true IF
|
||||
# TEMPORARY_DATA were true. """
|
||||
# if isinstance(query, basestring):
|
||||
# return self.select_if_string(query, temporary_data)
|
||||
# else:
|
||||
# return self.select_if_obj(query, temporary_data)
|
||||
|
||||
def explain(self, query, tablenames=None, find_all=False, target=None):
|
||||
""" Event handler for explanations. Given a ground query and
|
||||
a collection of tablenames that we want the explanation in
|
||||
|
|
@ -1232,17 +1157,37 @@ class Runtime (object):
|
|||
else:
|
||||
return self.delete_obj(formula, self.get_target(target))
|
||||
|
||||
def remediate(self, formula, target=None):
|
||||
""" Event handler for remediation. """
|
||||
if isinstance(formula, basestring):
|
||||
return self.remediate_string(formula, self.get_target(target))
|
||||
elif isinstance(formula, tuple):
|
||||
return self.remediate_tuple(formula, self.get_target(target))
|
||||
else:
|
||||
return self.remediate_obj(formula, self.get_target(target))
|
||||
|
||||
# Maybe implement one day
|
||||
# def select_if(self, query, temporary_data):
|
||||
# """ Event handler for hypothetical queries. Returns the set of
|
||||
# all instantiated QUERYs that would be true IF
|
||||
# TEMPORARY_DATA were true. """
|
||||
# if isinstance(query, basestring):
|
||||
# return self.select_if_string(query, temporary_data)
|
||||
# else:
|
||||
# return self.select_if_obj(query, temporary_data)
|
||||
|
||||
############### Internal interface ###############
|
||||
## Translate different representations of formulas into
|
||||
## the compiler's internal representation.
|
||||
## Only arguments allowed to be strings are suffixed with _string
|
||||
## the compiler's internal representation and then invoke
|
||||
## appropriate theory's version of the API.
|
||||
## Arguments that are strings are suffixed with _string.
|
||||
## All other arguments are instances of Theory, Atom, etc.
|
||||
|
||||
def select_obj(self, query, theory):
|
||||
return theory.select(query)
|
||||
|
||||
def select_string(self, policy_string, theory):
|
||||
policy = compile.get_parsed(['--input_string', policy_string])
|
||||
policy = compile.parse(policy_string)
|
||||
assert len(policy) == 1, \
|
||||
"Queries can have only 1 statement: {}".format(
|
||||
[str(x) for x in policy])
|
||||
|
|
@ -1256,10 +1201,9 @@ class Runtime (object):
|
|||
return theory.explain(query, tablenames, find_all)
|
||||
|
||||
def explain_string(self, query_string, tablenames, find_all, theory):
|
||||
policy = compile.get_parsed([query_string, '--input_string'])
|
||||
policy = compile.parse(query_string)
|
||||
assert len(policy) == 1, "Queries can have only 1 statement"
|
||||
results = self.explain_obj(policy[0], tablenames, find_all, theory)
|
||||
logging.debug("explain_obj results: " + iterstr(results))
|
||||
return compile.formulas_to_string(results)
|
||||
|
||||
def explain_tuple(self, tuple, tablenames, find_all, theory):
|
||||
|
|
@ -1270,7 +1214,7 @@ class Runtime (object):
|
|||
return theory.insert(formula)
|
||||
|
||||
def insert_string(self, policy_string, theory):
|
||||
policy = compile.get_parsed([policy_string, '--input_string'])
|
||||
policy = compile.parse(policy_string)
|
||||
# TODO: send entire parsed theory so that e.g. self-join elim
|
||||
# is more efficient.
|
||||
for formula in policy:
|
||||
|
|
@ -1284,11 +1228,60 @@ class Runtime (object):
|
|||
theory.delete(formula)
|
||||
|
||||
def delete_string(self, policy_string, theory):
|
||||
policy = compile.get_parsed([policy_string, '--input_string'])
|
||||
policy = compile.parse(policy_string)
|
||||
for formula in policy:
|
||||
self.delete_obj(formula, theory)
|
||||
|
||||
def delete_tuple(self, tuple, theory):
|
||||
self.delete_obj(compile.Atom.create_from_iter(tuple), theory)
|
||||
|
||||
def remediate_obj(self, formula, theory):
|
||||
""" Find a collection of action invocations that if executed
|
||||
result in FORMULA becoming false. """
|
||||
actionth = self.theory[self.ACTION_THEORY]
|
||||
classifyth = self.theory[self.CLASSIFY_THEORY]
|
||||
# look at FORMULA
|
||||
if isinstance(formula, compile.Atom):
|
||||
output = formula
|
||||
elif isinstance(formula, compile.Rule):
|
||||
output = formula.head
|
||||
else:
|
||||
assert False, "Must be a formula"
|
||||
# grab a single proof of FORMULA in terms of the base tables
|
||||
base_tables = classifyth.base_tables()
|
||||
proofs = classifyth.explain(formula, base_tables, False)
|
||||
if proofs is None: # FORMULA already false; nothing to be done
|
||||
return []
|
||||
# Extract base table literals that make that proof true.
|
||||
# For remediation, we assume it suffices to make any of those false.
|
||||
# (Leaves of proof may not be literals or may not be written in
|
||||
# terms of base tables, despite us asking for base tables--
|
||||
# because of negation.)
|
||||
leaves = [leaf for leaf in proofs[0].leaves()
|
||||
if (isinstance(leaf, compile.Literal) and
|
||||
leaf.table in base_tables)]
|
||||
logging.debug("Leaves: {}".format(iterstr(leaves)))
|
||||
# Query action theory for abductions of negated base tables
|
||||
actions = actionth.select(compile.parse1('action(x)'))
|
||||
actions = [action.arguments[0].name for action in actions]
|
||||
results = []
|
||||
for lit in leaves:
|
||||
goal = lit.make_positive()
|
||||
if lit.is_negated():
|
||||
goal.table = goal.table + "+"
|
||||
else:
|
||||
goal.table = goal.table + "-"
|
||||
# return is a list of goal :- act1, act2, ...
|
||||
# Turn it into a list of output :- act1, act2, ...
|
||||
for abduction in actionth.abduce(goal, actions, False):
|
||||
results.append(compile.Rule(output, abduction.body))
|
||||
return results
|
||||
|
||||
def remediate_string(self, policy_string, theory):
|
||||
policy = compile.parse(policy_string)
|
||||
assert len(policy) == 1, "Queries can have only 1 statement"
|
||||
return compile.formulas_to_string(self.remediate_obj(policy[0], theory))
|
||||
|
||||
def remediate_tuple(self, tuple, theory):
|
||||
self.remediate_obj(compile.Atom.create_from_iter(tuple), theory)
|
||||
|
||||
|
|
|
|||
|
|
@ -37,11 +37,11 @@ class TestRuntime(unittest.TestCase):
|
|||
run.delete(tuple(alist))
|
||||
|
||||
def string_to_database(self, string):
|
||||
c = compile.get_compiled([string, '--input_string'])
|
||||
formulas = compile.parse(string)
|
||||
database = runtime.Database()
|
||||
for atom in c.theory:
|
||||
if atom.is_atom():
|
||||
database.insert(atom)
|
||||
for formula in formulas:
|
||||
if formula.is_atom():
|
||||
database.insert(formula)
|
||||
return database
|
||||
|
||||
def check_db_diffs(self, actual, correct, msg):
|
||||
|
|
@ -86,8 +86,8 @@ class TestRuntime(unittest.TestCase):
|
|||
if equal is None:
|
||||
equal = lambda x,y: x == y
|
||||
logging.debug("** Checking equality: {} **".format(msg))
|
||||
actual = compile.get_parsed([actual_code, '--input_string'])
|
||||
correct = compile.get_parsed([correct_code, '--input_string'])
|
||||
actual = compile.parse(actual_code)
|
||||
correct = compile.parse(correct_code)
|
||||
extra = minus(actual, correct)
|
||||
missing = minus(correct, actual)
|
||||
self.output_diffs(extra, missing, msg)
|
||||
|
|
@ -507,8 +507,8 @@ class TestRuntime(unittest.TestCase):
|
|||
if unifier2 is None:
|
||||
# logging.debug("Generating new unifier2")
|
||||
unifier2 = runtime.TopDownTheory.new_bi_unifier()
|
||||
p1 = compile.get_parsed([atom_string1, '--input_string'])[0]
|
||||
p2 = compile.get_parsed([atom_string2, '--input_string'])[0]
|
||||
p1 = compile.parse(atom_string1)[0]
|
||||
p2 = compile.parse(atom_string2)[0]
|
||||
changes = unify.bi_unify_atoms(p1, unifier1, p2, unifier2)
|
||||
self.assertTrue(changes is not None)
|
||||
print_unifiers(changes)
|
||||
|
|
@ -555,8 +555,8 @@ class TestRuntime(unittest.TestCase):
|
|||
self.open(msg)
|
||||
unifier1 = runtime.TopDownTheory.new_bi_unifier()
|
||||
unifier2 = runtime.TopDownTheory.new_bi_unifier()
|
||||
p1 = compile.get_parsed([atom_string1, '--input_string'])[0]
|
||||
p2 = compile.get_parsed([atom_string2, '--input_string'])[0]
|
||||
p1 = compile.parse(atom_string1)[0]
|
||||
p2 = compile.parse(atom_string2)[0]
|
||||
changes = unify.bi_unify_atoms(p1, unifier1, p2, unifier2)
|
||||
if changes is not None:
|
||||
logging.debug(
|
||||
|
|
@ -572,7 +572,7 @@ class TestRuntime(unittest.TestCase):
|
|||
def test_same(self):
|
||||
""" Test whether the SAME computation is correct. """
|
||||
def str2form(formula_string):
|
||||
return compile.get_parsed([formula_string, '--input_string'])[0]
|
||||
return compile.parse(formula_string)[0]
|
||||
def assertIsNotNone(x):
|
||||
self.assertTrue(x is not None)
|
||||
def assertIsNone(x):
|
||||
|
|
@ -840,14 +840,21 @@ class TestRuntime(unittest.TestCase):
|
|||
logging.debug(run.explain("p(1)"))
|
||||
# self.fail()
|
||||
|
||||
def test_nonrecursive_explain(self):
|
||||
""" Test explanations for NonrecursiveRuleTheory. """
|
||||
def test_nonrecursive_abduction(self):
|
||||
""" Test abduction for NonrecursiveRuleTheory. """
|
||||
def check(query, code, tablenames, correct, msg, find_all=True):
|
||||
# We're interacting directly with the runtime's underlying
|
||||
# theory b/c we haven't yet decided whether Abduce should
|
||||
# be a top-level API call.
|
||||
actth = runtime.Runtime.ACTION_THEORY
|
||||
run = self.prep_runtime()
|
||||
actiontheory = run.theory[actth]
|
||||
run.insert(code, target=actth)
|
||||
actual = run.explain(query, tablenames=tablenames,
|
||||
find_all=find_all, target=actth)
|
||||
query = compile.parse(query)
|
||||
actual = actiontheory.abduce(query[0], tablenames=tablenames,
|
||||
find_all=find_all)
|
||||
# convert result to string, since check_same expects strings
|
||||
actual = compile.formulas_to_string(actual)
|
||||
self.check_same(actual, correct, msg)
|
||||
|
||||
code = ('p(x) :- q(x), r(x)'
|
||||
|
|
@ -917,12 +924,53 @@ class TestRuntime(unittest.TestCase):
|
|||
'p(x) :- q(x,2) p(x) :- q(x,2)',
|
||||
"Existential variables that do not become ground")
|
||||
|
||||
code = ('p(x) :- q(x), r(z)'
|
||||
code = ('p+(x) :- q(x), r(z)'
|
||||
'r(z) :- s(z), q(x)'
|
||||
's(1)')
|
||||
check('p(x)', code, ['q'],
|
||||
'p(x) :- q(x), q(x1)',
|
||||
check('p+(x)', code, ['q'],
|
||||
'p+(x) :- q(x), q(x1)',
|
||||
"Existential variables with name collision")
|
||||
|
||||
def test_remediation(self):
|
||||
"""Test remediation computation"""
|
||||
def check(action_code, classify_code, query, correct, msg):
|
||||
run = self.prep_runtime()
|
||||
actth = run.ACTION_THEORY
|
||||
clsth = run.CLASSIFY_THEORY
|
||||
run.insert(action_code, target=actth)
|
||||
run.insert(class_code, target=clsth)
|
||||
self.showdb(run)
|
||||
self.check_equal(run.remediate(query), correct, msg)
|
||||
|
||||
# simple
|
||||
action_code = ('action("a")'
|
||||
'p-(x) :- a(x)')
|
||||
class_code = ('err(x) :- p(x)'
|
||||
'p(1)')
|
||||
check(action_code, class_code, 'err(1)', 'err(1) :- a(1)', 'Monadic')
|
||||
|
||||
# rules in action theory
|
||||
action_code = ('action("a")'
|
||||
'p-(x) :- q(x)'
|
||||
'q(x) :- a(x)')
|
||||
class_code = ('err(x) :- p(x)'
|
||||
'p(1)')
|
||||
check(action_code, class_code, 'err(1)', 'err(1) :- a(1)',
|
||||
'Monadic, indirect')
|
||||
|
||||
# multiple conditions in error
|
||||
action_code = ('action("a")'
|
||||
'action("b")'
|
||||
'p-(x) :- a(x)'
|
||||
'q-(x) :- b(x)')
|
||||
class_code = ('err(x) :- p(x), q(x)'
|
||||
'p(1)'
|
||||
'q(1)')
|
||||
check(action_code, class_code, 'err(1)',
|
||||
'err(1) :- a(1) err(1) :- b(1)',
|
||||
'Monadic, two conditions, two actions')
|
||||
|
||||
|
||||
|
||||
if __name__ == '__main__':
|
||||
unittest.main()
|
||||
|
|
|
|||
Loading…
Reference in New Issue