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.
Use coala with
-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).
This is an encoding of a spring loaded door (
sldoor_c) written in C without
<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.
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
More examples are available at: sourceforge svn
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
<where> expression after which the variable
Switch can be defined
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.
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
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.
Starting from v0.5 it is possible to generate incremental problem encodings
that can be solved incrementally by using
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
Use coala with
-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
The fluent names
g are a shorthand for conjunctions of fluents of the
<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.
<executable> a <if> f.
<impossible> a <if> f.
Description of initial state
Description of goal state
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.
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
The coala tool used with the option
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.
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.
<fluent> f_1,f_2,f_3.instead of
f_1,f_2,f_3 <at> 0.
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.
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
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.
% 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