coala
coala is a versatile compiler from action languages to answer set programs. It supports different encodings, variables and LTL style queries.

Coala

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.

Overview

Options of Coala Toolchain Script 

Usage: coala [options] file [number]

Options:
  -l LANG, --language=LANG
                        the action language (c, c_taid, b, al or m) to be used
                        as input (default: c)
  -s FILE, --static-file=FILE
                        file containing static information such as variable
                        types.
  -c t=v, --const=t=v   replaces constant t with value v
  -d, --debug           show debugging output
  --version             show program's version number and exit
  -h, --help            show this help message and exit

  Encoding Options:
    -i INC, --incremental=INC
                        use incremental encoding. INC can be yes, no or
                        backwards. Default: yes
    -e, --meta-encoding
                        use meta-encoding
    -n, --negation      simulate classical negation instead of using the
                        built-in one

  Solver Options:
    --max-sol=NUM       Compute [number] solutions. Default: 1
    --imax=NUM          Perform at most NUM incremental steps. Default: 99
    -t, --text          show only coala output and don't look for solutions
    -g, --ground        show only grounded coala output and don't look for
                        solutions

  Output Options:
    -o OUTPUT, --output=OUTPUT
                        change the way the solutions are presented, long,
                        compact or raw. Default: compact
    -f, --show-fluents  show not only actions, but also fluents in solution

Options of Coala Binary

The usage of coala and all possible options are stated below. If no input file is given, it reads from STDIN. 
Usage: coala.bin [-l|--language=<LANG>] [-i|--incremental] [-r|--reverse] [-d|--debug=<num>]
             [-e|--no-direct-enc] [-w|--no-where] [-n|--neg] [--help] [<file>]

  -l, --language=<LANG>    the action language (c, c_taid or m) to be used as input (default: c)
  -i, --incremental        output incremental encoding (does not work with -l c_taid)
  -r, --reverse            output reverse encoding (does not work with -l c_taid)
  -d, --debug=<num>        debug program by showing more atoms (default: 0)
  -e, --no-direct-enc      don't output direct encoding to ASP (does not work with -l c_taid)
  -w, --no-where           do not check for correct <where> clauses
  -n, --neg                simulate classical negation instead of using the built-in one
  -h, --help               print help information and exit
A debug level of 0 means that only actions are shown in the answer sets. Level 1 also shows fluents and level 2 shows even more.

Please note that the -e option is not lparse compatible. Please use a gringo based system to process this output.

Benchmarks

There has been an extensive benchmark study with all of coala's options to figure out which combination of options provides the best results. The winner was the -in option. For more details see the separate page.

Simulated Classical Negation vs. Built-in Classical Negation

The standard behavior of coala is to use lparse's built-in classical negation in the output. This might allow for faster processing and optimization by lparse which has to be called using the --true-negation command line parameter.

The command line option -n or --neg of coala switches to simulated classical negation in the output. Resulting programs are working "out of the box" without the need to specify additional parameters with the grounder. Whether this makes any difference in performance is subject to further research.
Negative actions and fluents are then recognized by the prefix neg_. Rules like :- fluent, neg_fluent. are added to ensure that a fluent and its negation can not hold in the same state.

Attention! When using lparse and classical negation, you have to call lparse with the --true-negation option.

Download

Attention! New versions can be downloaded from Sourceforge

Version 1.0.1
64bit GNU/Linux binary | 32bit GNU/Linux binary | source code

Version 1.0.0
64bit GNU/Linux binary | 32bit GNU/Linux binary | source code

Version 0.9.5
64bit GNU/Linux binary | 32bit GNU/Linux binary | source code

Version 0.9.4
64bit GNU/Linux binary | 32bit GNU/Linux binary | source code

Version 0.9.3
64bit GNU/Linux binary | 32bit GNU/Linux binary | source code

Version 0.9.2
64bit GNU/Linux binary | 32bit GNU/Linux binary | source code

Version 0.9.1
Reimplementation and renamed from al2asp to coala
64bit GNU/Linux binary | 32bit GNU/Linux binary | source code

Version 0.5
64bit GNU/Linux binary | 32bit GNU/Linux binary | source code

Version 0.4
64bit GNU/Linux binary | 32bit GNU/Linux binary | source code

Version 0.3
32bit GNU/Linux binary | source code

Version 0.2
32bit GNU/Linux binary | source code

Version 0.1
32bit GNU/Linux binary | source code

The latest source code can be found in the public SVN repository. Bug reports and patches are welcome.

Change Log 

version 1.0.1 (2010/11/11):
    general:
    * compatible with gringo v3
    * changed copyright information for program opts

version 1.0.0 (2010/07/28):
    general:
    * does not need to link against flex anymore
    * fixed some bugs in coala wrapper script about clingo usage and output
      formatting

version 0.9.5 (2010/05/07):
    general:
    * added support for action language B and A_L
    * added wrapper script for easier usage of coala toolchain
    * types in <where> part of rules can now be negated using 'not'

    * all information from <where> part is now added to the program

    action language C:
    * fixed segfault with causes rules
    * fixed compilation bug for static rules without <if> part

version 0.9.4 (2010/02/22):
    action language C:
    * added experimental incremental LTL encoding (direct and non-direct)

version 0.9.3 (2010/01/27):
    general:
    * multiple input files can be given via command line
    * compiling Coala without flex and bison++ is now easier

    action language C:
    * LTL queries can now be used with direct encoding
    * multiple LTL queries are now treated as disjunctions of one query
    * fixed bug with LTL so that you can now query for actions as well
    * LTL is now standard compliant and tries to find counterexamples
    * LTL queries now handle idle states properly
    * fixed bug where conjunctions of fluents (composite fluents) could not be
      caused in non-direct encoding
    * fixed bug where negation of LTL auxiliary functions was done improperly
    * added biocham LTL example
    * added warning for queries that may cause problems with reverse
      incremental encoding
    * fixed monkey and water example for reverse incremental encoding
    * fixed segfault when defining negative fluents
    * fixed small bug in yale shooting example

version 0.9.2 (2009/11/11):
   general:
   * coala now offers the library libcoala
   * instructions on how to build without flex and bison++

   action language C:
   * fixed bug where types for variables from constraints were not checked
     and not included
   * new Towers of Hanoi example
   * modified ferryman example for scalability
   * fixed biocham_mapk example for gringo compatibility

version 0.9.1 (2009/07/01):
   general:
   * reimplementation of al2asp and renamed to coala
   * new bugs might have been introduced

   action language C:
   * added pooling of variables in definitions, e.g. var(X;Y)
   * function symbols as arguments of fluents and action
   * experimental support for LTL-like queries
   * new non-direct encoding
   * experimental support for reverse incremental solving
   * new parameter to suppress type checking of variables

version 0.5 (2008/10/22):
   general:
   * changed default language to C
   * added three examples (blocksworld, ferryman, monkeys)

   action language C:
   * support for gringo's incremental grounding

version 0.4 (2008/07/14):
   general:
   * changed Buildsystem to CMake
   * added several examples
   * added undocumented and unsupported C to C_taid translation

   action language C:
   * support for query language R (<occurs at>, <holds at>

     and hypothetical query)
   * support for constants to variable handling
   * support for addition in constraints
   * prevented actions form occurring in last time step (T<n)
   * fixed bug in variable handling
   * fixed bug where static rules were only grounded till n-1

   action language C_taid:
   * changed end time from latest observation to parameter n
   * fixed time problem with prediction
   * fixed default fluent bug
   * fixed negative action observations bug

version 0.3 (2007/10/21):
   general:
   * added support for file input in addition to STDIN
   * changed debug level behaviour
   * debug level 0 shows only actions and 1 also fluents
   * default is now debug level 1
   * added one example for action language C

   action language C:
   * rewrite of most code for simplicity and modularity
   * added experimental support for variables with <where>

   action language C_taid:
   * removed <at> for specifying max_time in queries
   * specify it with lparse -c n=[max_time]

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). The shortcuts defined in Action Languages (section 6 / p. 8-9) are present since version 0.2 and variables have been implemented in version 0.3.

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: http://sourceforge.net/p/potassco/code/HEAD/tree/trunk/coala/examples/c/

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).

#hide reaction(X).
#hide product(X).
#hide input(X1,X2).
#hide output(X1,X2).
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.

Definitions 


<fluent> f.
<action> a.

Defined fluents for AL 

<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 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

  • 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 CTAID 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 which were implemented in the project Bounded Model Checking and Causal Languages. They work for description 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 & b.

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

%LTL: G !c.
%LTL: G ! F (a & b).    % from t>2
%LTL: !(a | b) U !c.    % from t>0
%LTL: !a U X(a&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