- Action Language C
- Action Language B and AL
- Action Language CTAID
- LTL Queries
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
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 exitA 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
-eoption is not lparse compatible. Please use a gringo based system to process this output. extensive benchmark study with all of coala's options to figure out which combination of options provides the best results. The winner was the
-inoption. For more details see the separate page.
--true-negationcommand line parameter. The command line option
--negof 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-negationoption. 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.
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]
-l cor 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.
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.
coala.bin sldoor_c | clingo -c t=2 0This 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=xoption where
xis the maximum number of state transitions. More examples are available at: http://sourceforge.net/p/potassco/code/HEAD/tree/trunk/coala/examples/c/
on(Switch). The type of the variables has to be defined, too. This is done by using a
<where>expression after which the variable
Switchcan 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 0It is also possible to use constraints like
<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.
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
-nswitch because the gringo part of iclingo still does not handle classical negation correctly in combination with incremental output.
-l bto 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.
gare a shorthand for conjunctions of fluents of the form
<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. 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
-l c_taidtranslates 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.
<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
- 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
ato 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
<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>3You can run this example by executing
coala.bin -d1 ltl_two_bit_counter.alc | clingo -c t=1The 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