Command-Line Mode

The GOAL command-line mode can be either single mode or batch mode. In the single mode, only one command can be executed each time. In the batch mode a sequence of commands can be executed. A single command is an instr while a sequence of command is a block in the grammar rules (see the GRAMMAR section).

To execute a single command, the command should be preceded by "java -jar goal_????_??_??.jar " (with ????_??_?? replaced by an appropriate release date). An input automaton must be in the .gff format. A .gff file contains type information of the automaton it describes.

To execute a sequence of commands, you can write GOAL scripts. For example, suppose the file SCRIPT contains a sequence of commands. You can run these commands by executing "java -jar goal_????_??_??.jar batch SCRIPT". Unlike the execution of a single command, in a GOAL script, variables can be used to capture the result of commands.

Table of Contents

Grammar Variables Lists Arrays Multiple Assignments Statements Commands for Automata Commands for Formulae Other Commands Examples List of All Commands

GRAMMAR

block := ( stmt )*

stmt := instr ";" | for_stmt | if_stmt

instr :=
    "echo" ( -n )? ( expr )?
  | "save" lval file_or_lval
  | "load" lval file_or_lval
  | "batch" file_or_lval
  | "interactive"
  | "exit"
  | "break" ( expr )?
  | "continue" ( expr )?
  | lval "=" ( expr | cmd_expr )
  | "(" lval ( "," lval )* ")" "=" ( expr | cmd_expr )
  | cmd_expr

for_stmt := "for" lval "in" expr "do" block "done"

if_stmt := ( "if" expr "then" block ) ( "elif" expr "then" block )* ( "else" block )? "fi"

cmd_expr :=
    emptiness_expr
  | containment_expr
  | equivalence_expr()
  | convert_expr()
  | intersection_expr()
  | union_expr()
  | complement_expr()
  | determinable_expr()
  | determinization_expr()
  | minimization_expr()
  | simplify_expr()
  | reduce_expr()
  | prunefairset_expr()
  | promela_expr()
  | stat_expr()
  | import_expr()
  | genautomaton_expr()
  | translate_expr()
  | validity_expr()
  | satisfiability_expr()
  | genformula_expr()
  | hierarchy_expr()
  | readline_expr()
  | open_expr()
  | close_expr()
  | split_expr()
  | seq_expr()
  
emptiness_expr := "emptiness" file_or_lval

containment_expr := "containment" ( -m containment_alg )* file_or_lval file_or_lval

equivalence_expr := "equivalence" file_or_lval file_or_lval

convert_expr := "convert" ( -t automaton_type | -o file_or_lval )* file_or_lval

intersection_expr := "intersection" ( -o file_or_lval )? file_or_lval file_or_lval

union_expr := "union" ( -o file_or_lval )? file_or_lval file_or_lval

complement_expr := 
  "complement" ( -m complement_alg | -o file_or_lval | -s expr | -t expr | 
  -eq | -r | -tt | -bfs | -madj | -eg | -cp | -tr | -ro | -macc )* file_or_lval

determinable_expr :=
  "determinable" file_or_lval

determinization_expr :=
  "determinization" ( -m determinization_alg | -o file_or_lval )* file_or_lval

minimization_expr := "minimization" ( -o file_or_lval )? file_or_lval

simplify_expr := "simplify" ( -o file_or_lval )? file_or_lval

reduce_expr := "reduce" ( -o file_or_lval )? file_or_lval

prunefairset_expr := "prunefairset" ( -o file_or_lval )? file_or_lval

promela_expr := "promela" ( -o file_or_lval )? file_or_lval

stat_expr := "stat" ( -s | -t )? file_or_lval

import_expr := "import" ( -p external_program )? file_or_lval

genautomaton_expr := 
  "genautomaton" ( -t automaton_type | -s expr | -n expr | -pt expr |
  -ps expr | -pa expr | -r | -S )* 

hierarchy_expr :=
  "hierarchy" formula_or_lval

translate_expr := 
  "translate" ( -m translate_alg | -t automaton_type | -o file_or_lval )* 
  formula_or_lval

validity_expr := "validity" formula_or_lval

satisfiability_expr := "satisfiability" formula_or_lval

genformula_expr := 
  "genformula" ( -l expr | -n expr | -w int_or_lval int_or_lval int_or_lval |
  -r | -of | -mcp | int_or_lval )*

readline_expr := "readline" file_or_lval

open_expr := "open" file_or_lval

close_expr := "close" int_or_lval

split_expr := "split" ( -d string_or_lval )? ( expr | cmd_expr )

seq_expr := "seq" expr ( expr )? ( expr )?

complement_alg :=
    "ramsey" | "safra" | "wapa" | "waa" | "piterman" | "ms"
  | "modifiedsafra" | "modsafra" | "kurshan" | "rank" | "slice" | lval

containment_alg :=
  "default" | "rank"

determinization_alg :=
  "classic" | "safra" | "modifiedsafra" | "ms" | "piterman" | lval
	
translate_alg :=
    "tableau" | "temporaltester" | "tester" | "inctableau" | "gpvw"
  | "gpvw+" | "ltl2aut" | "ltl2aut+" | "ltl2ba" | "pltl2ba" | "couvruer"
  | "ltl2buchi" | "ltl2buchiplus" | "modella" | lval

automaton_type := 
    "nbw" | "ngbw" | "nmw" | "nrw" | "nsw" | "npw" 
  | "ntbw" | "ntgbw" | "ntmw" | "ntrw" | "ntsw" | "ntpw" | "classic" 
  | "vwaa" | lval

external_program := "modella" | "ltl2buchi" | lval

expr :=
    expr ( "\/" | "|" ) expr
  | expr ( "/\" | "&" ) expr
  | expr "==" expr
  | expr "!=" expr
  | expr "<" expr
  | expr ">" expr
  | expr "<=" expr
  | expr ">=" expr
  | expr "+" expr
  | expr "-" expr
  | expr "*" expr
  | expr "/" expr
  | expr "%" expr
  | "-" expr
  | "!" expr
  | number
  | bool
  | string
  | lval
  | "time"
  | "(" expr ")"
  | "`" shell_cmd "`"
  
number := int | float

formula_or_lval := string | lval

file_or_lval := file | string

int_or_lval := int | lval

string_or_lval := string | lval

bool := "true" | "false"

lval := "$" id

int := (["0"-"9"])+

float := (["0"-"9"])+ "." (["0"-"9"])+

file := (["a"-"z","A"-"Z","0"-"9","_","-",".","/"])+

id := ["a"-"z","A"-"Z"] ( ["a"-"z","A"-"Z","0"-"9","_"] )*

shell_cmd := ( ~["`","\n","\r"] )*

VARIABLES

In GOAL scripts, every variable name should start with "$". You don't need to declare the type of a variable before using it. For example, below are some acceptable variable names:

  $var
  $v0
  $v_0

LISTS

The only way to create a list is to execute the readline command which reads a file line by line. Each element in the list is a line in the file. For example, the following statement will read the file "input" and put each line as an element in the list variable $list.

  $list = readline "input";

ARRAYS

An array is a map from an object convertible to a string to an object. Basically, you can use any object as the index of an array. For example, the following commands are acceptable.

  $arr[0] = 0;
  $arr["number"] = 10;

MULTIPLE ASSIGNMENTS

A multiple assignment tries to split an object and assign the results to a set of variables. Note that the number of left elements should be less than or equal to the number of right elements. A string can be split by spaces, tabs, and newlines. For example, the following statement will split the string into "1" and "2". If you want to use delimiters rather than spaces, tabs, and newlines, you can use the split command.

  ($x, $y) = "1 2";

  ($elm_1, $elm_2, ..., $elm_n) = $list

  ($key_1, $key_2, ..., $key_n) = $arr
  $arr[$key_1] = 0;
  $arr[$key_2] = 1;
  ...

STATEMENTS

A statement can be an instruction (command) with a trailing ";", a for-statement, or an if-statement. A for-statement iterates on the elements of a list or the key set of an array. For examples, below is a for-statements which iterates on a list.

  $list = readline "input";
  for $elm in $list do
    echo $elm;
  done

  for $key in $arr do
    echo $arr[$key];
  done

SHELL COMMANDS

A shell command can be invoked by putting the command between two `. For example, the following command will invoke the shell command "seq 1 10" and the variable $x will capture both the standard output and the error output of this shell command.

  $x = `seq 1 10`;

Below is another example that prints numbers from 1 to 10 on the screen.

  for $x in `seq 1 10` do
    echo $x;
  done

COMMANDS FOR AUTOMATA

COMMANDS FOR FORMULAE

OTHER COMMANDS

EXAMPLES

#!./goal batch

echo "Translate random generated formulae by various translation algorithms.";
echo;

$algorithms = "tester inctableau gpvw ltl2aut+ ltl2ba";
$formulae = genformula -n 2 -l 5 -w 1 1 0 10;
$count = 1;
for $formula in $formulae do
  echo "#" + $count + ": Translating " + $formula;
  for $alg in $algorithms do
    echo "  by " + $alg;
    $ti = time;
    $o = translate -m $alg $formula;
    $ti = time - $ti;
    ($s, $t) = stat $o;
    echo "    # of states: " + $s;
    echo "    # of transitions: " + $t;
    echo "    time: " + $ti;
    $ret_st[$alg] = $ret_st[$alg] + $s;
    $ret_tr[$alg] = $ret_tr[$alg] + $t;
    $ret_ti[$alg] = $ret_ti[$alg] + $ti;
  done
  $count = $count + 1;
done

echo;
echo "========== Statistics ==========";
for $alg in $algorithms do
  echo $alg + ":";
  echo "  # of states: " + $ret_st[$alg];
  echo "  # of transitions: " + $ret_tr[$alg];
  echo "  time: " + $ret_ti[$alg];
done

LIST OF ALL COMMANDS

Below is the list of commands.

• Commands for automata:
  • emptiness
  • containment
  • equivalence
  • convert
  • intersection
  • union
  • complement
  • determinable
  • determinization
  • simplify
  • reduce
  • prunefairset
  • stat
  • import
  • genautomaton
  • promela
• Commands for formulae:
  • translate
  • validity
  • satisfiability
  • genformula
  • hierarchy
• Other commands:
  • echo
  • save
  • load
  • batch
  • interactive
  • exit
  • break
  • continue
  • split
  • seq
  • time
  • readline
  • open
  • close
  • help