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 A_L, B, C, a subset of C+ and the action language C_TAID. 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.

• Attention! When using lparse and classical negation, you have to call lparse with the --true-negation option.
• Attention! The translator and examples have been written for lparse or gringo/clingo 2 and 3. There might be problems with newer gringo versions.

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 A_L

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.

• Definitions

  <fluent> f.
  <action> a.
  

• Defined fluents for A_L

  <defined fluent> f.
  

  Write this intead of <fluent> f. to have a defined fluent which is not inertial and obeys the closed world assumption.

• Static causal law

  f <if> g.
  

• Dynamic Causal law

  a <causes> f <if> g.
  

• Executability condition

  <executable> a <if> f.
  

• Impossibility condition

  <impossible> a <if> f.
  

• Description of initial state

  <initially> f.
  

• Description of goal state

  <goal> f.
  

  Please note that using multiple <goal> statements specifies alternative goals. If you just want one goal, just use one <goal> statement and use a conjunction of fluents.

• Using variables works analog to C

  <fluent> f(X) <where> domain(X).
  

• Furthermore, the queries that are available for action language C can also be used for B.

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 C_TAID

The coala tool used with the option --language=c_taid or -l c_taid translates the action language C_TAID. 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 C_TAID.

<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

• written in C++ using flex and bison++ instead of java
• it only does the translation; no grounding, solving or visualization is done
• a dot . is used to end every C_TAID rule
• actions and fluents can be defined with lists e.g. <fluent> f_1,f_2,f_3. instead of <fluent> f_1., <fluent> f_2. and <fluent> f_3.
• the same holds for all observations e.g. f_1,f_2,f_3 <at> 0.
• there are no parameters for the kind of the query
• all queries are directly in the input file
• the output isn’t separated into several files for direct progression to grounding
• there is the trig_ prefix instead of the trigger_ prefix in the output

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