Overview

The coala tool translates an action language into a logic program under the answer set semantics. After being grounded by lparse or gringo, the logic program can be solved by an answer set solver such as clasp. At the moment coala is able to translate the action language AL, B, C, a subset of C+ and the action language CTAID. The type of input language can be specified with a command line option.

The coala system can be downloaded from sourceforge. The latest source code can also be found on sourceforge. Bug reports and patches are welcome.

Action Language C

Use coala with --language=c, -l c or no language option to get a translation from action language C. Static and dynamic laws were introduced in version 0.1 and are translated according to Representing Transition Systems by Logic Programs (section 4).

Example Input

This is an encoding of a spring loaded door (sldoor_c) written in C without variables.

<action> openDoor.
<fluent> closed.

<caused> closed <if> closed.

<caused> -closed <if> <true> <after> openDoor.

Attention! Action and fluent names have to start with a lowercase letter.

Example program call

coala.bin sldoor_c | clingo -c t=2 0

This command line translates the spring loaded door example into a logic program which is instantly grounded and solved by the hybrid program clingo (gringo + clasp) which lists all solutions (0).

Attention! When translating from action language C, you have to call lparse with the -c t=x option where x is the maximum number of state transitions.

More examples are available at: sourceforge svn

Variables in C

Since version 0.3 actions and fluents can have variables. They are added by using parentheses after the fluent or action name and have to start with an uppercase letter and are separated by commas. E.g. put(Entity, Location) and on(Switch). The type of the variables has to be defined, too. This is done by using a <where> expression after which the variable Switch can be defined like switch_type(Switch). For coala this is sufficient, but if you want to actually use the output, you have to provide a second file to the grounder where the types are specified like facts in an ASP program. E.g. switch_type(switch1). switch_type(switch2).

The following is a simple example program (biocham.alc) with variables.

% preamble
<action> occurs(X) <where> reaction(X).
<fluent> on(X) <where> product(X).

% produce output
<caused> on(P) <after> occurs(R) <where> reaction(R),product(P),output(R,P).
% force inputs to be present
<caused> <false> <after> occurs(R),-on(P) <where> reaction(R),product(P),input(R,P).

% inputs maybe consumed
occurs(R) <may cause> on(P),-on(P) <if> on(P) <where> reaction(R),product(P),input(R,P).

% inertia
<inertial> on(P), -on(P) <where> product(P).

A file ( biocham.stat) specifying the variables could look like this

reaction(r1).

product(a).
product(b).

input(r1,a).
output(r1,b).

Using these two files, answer sets can now be computed using this command line: coala.bin biocham.alc | cat - biocham.stat | clingo -c t=1 0

It is also possible to use constraints like X>=Y after the <where> expression.

Attention! The variable T is used internally for tracking the current time. You are allowed to use it, but do it with caution in order to prevent unexpected results.

Incremental Encodings

Starting from v0.5 it is possible to generate incremental problem encodings that can be solved incrementally by using iclingo.

An example command line looks like that:

coala.bin -i -n bw.alc | cat - bw.stat | iclingo 0

Note that you have to use the -n switch because the gringo part of iclingo still does not handle classical negation correctly in combination with incremental output.

Action Language B and AL

Use coala with --language=b or -l b to get a translation from action language B or AL. The encoding is based on the one described in Domain-Dependant Knowledge in Answer Set Planning.

Syntax

The fluent names f and g are a shorthand for conjunctions of fluents of the form f1,...,fn.

Examples

You can find several examples in the public SVN repository. Use the following commands to run them.

coala.bin -l b -i blocksworld.alb | cat - blocksworld.stat | iclingo 0
coala.bin -l b -i briefcase.alb | iclingo 0
coala.bin -l b -i bulldozer.alb | cat - bulldozer.stat | iclingo 0
coala.bin -l b -i crossing.alb | cat - crossing.stat | iclingo 0
coala.bin -l b -i ignite.alb | cat - ignite.stat | iclingo 0
coala.bin -l b -i medicine.alb | iclingo 0

Action Language CTAID

The coala tool used with the option --language=c_taid or -l c_taid translates the action language CTAID. It takes a file containing an action description, action observations and a query as input or to STDIN and outputs a logic program to SDTOUT.

Example Input

This is the yale shooting example written in CTAID.

<action> shoot, load.
<fluent> alive, loaded.

load <causes> loaded.
shoot <causes> -alive <if> loaded.
shoot <causes> -loaded.

<noconcurrency> load, shoot.

-loaded <at> 0.
alive <at> 0.

<plan> -alive.

Differences to the BioNetReasoning Tool

LTL Queries

Since version 0.9.3 coala has experimental support for LTL queries. They work for descriptions in action language B and C. The queries ask if a certain property expressed by the LTL formula is true. This is done by using bounded model checking techniques which try to find counter examples that violate the property within the given bound. If Coala+Clingo does not return any answer sets, then there are no counter-examples within the bound.

Syntax

For technical reasons, the syntax of LTL formulas differs slightly from the syntax of action and fluent formulas. Assume a to be a LTL formula, then valid formulas are:

a := <true> | <false> | a | !a | (a & a) | (a | a) |
     X a | F a | G a | a U a | a W a | a R a

Example

The following example was found in “Bounded model checking using satisfiability solving, 2001” p. 7. It represents a two bit counter where a represents the left bit and b the right bit. The fluent c never changes its value and only present to better demonstrate certain queries. The system starts in state 00 (-a-b), then goes into state 01 (-ab), then 10 (a-b) and then into state 11 (ab). After that, the counter overflows and starts again from state 00. Here a loop starts.

<fluent> a,b,c.
<inertial> a, -a, b, -b, c, -c.

<caused> b <after> -b.
<caused> -b <after> b.

<caused> a <after> -a,b.
<caused> -a <after> a,b.

-a, -b, c <holds at> 0.

LTL: a.
%LTL: !a &#38; b.

%LTL: a | b.
%LTL: X (a &#38; b).    % from t>0
%LTL: ! F a.        % from t>1
%LTL: ! F(a &#38; b).   % from t>2

%LTL: G !c.
%LTL: G ! F (a &#38; b).    % from t>2
%LTL: !(a | b) U !c.    % from t>0
%LTL: !a U X(a&#38;b).  % never

%LTL: ! (b R !a).   % from t>0
%LTL: ! (!c R c).   % from t>3

You can run this example by executing coala.bin -d1 ltl_two_bit_counter.alc | clingo -c t=1.

The queries at the end of the example should produce a counter example showing that the property they describe is not true in the model/transition system. Some only do so if you run the example with a certain time bound that is given as a comment after the query.

Biocham Example

% preamble
<action> occurs(X) <where> reaction(X).
<fluent> on(X) <where> product(X).

% produce output

<caused> on(P) <after> occurs(R) <where> reaction(R),product(P),output(R,P).

% force inputs to be present
<caused> <false> <after> occurs(R),-on(P) <where> reaction(R),product(P),input(R,P).


% inputs maybe consumed
occurs(R) <may cause> -on(P) <where> reaction(R),product(P),input(R,P).

% inputs are always consumed
%<caused> -on(P) <after> occurs(R) <where> reaction(R),product(P),input(R,P).


% inertia
<inertial> on(P), -on(P) <where> product(P).

on(a) <holds at> 0.
-on(b) <holds at> 0.

LTL: on(a) & F (occurs(r1) & G on(b)).

This can be run with a biocham instance like this one using the following command:

coala.bin ltl_biocham.alc | cat - biocham.stat | clingo -c t=2 0