DSL for Constructing Goals and Tactics

‘DSL’ stands for Domain Specific Language.

Basic terminology. A goal can be given to an agent, and represents what the agent has to achieve/solve. A goal can also be a composition of other goals; this is called a goal-structure. A goal-structure can for example be composed of n goals which have to be solved in sequence.

A tactic is a program for solving a goal. Every leaf-goal in a goal structure must have a tactic associated with it. In turn, a tactic can be composed from actions. An action can be guarded, which defines if it is executable or not.

For explanation on how tactics are executed to solve a goal (or in other words: agents’ execution model), see this document .

Most of the contsructs below are defined in:

• AplibEDSL.java
• Iv4xrEDSL.java

Goal

The syntax of goals is shown below.

goal ::=

• goal( name ).toSolve( predicate ).withTactic( tactic )

A predicate is a Java-function that returns a boolean. It can be constructed using a lambda-expression. For example (int x) -> x==10 is a predicate that is true when given a integer value 10. If this predicate is used as a goal, it specifies when the goal is considered as solved.

A goal needs a tactic; it specifies how to solve it. The syntax of tactics is given later.

A goal-structure is a composition of goals, e.g. it can be a sequence of sub-goals that should be achieved in the order as the sequence specifies.

goal-structure ::=

• goal.lift()
• SUCESS( comment )
• FAIL( comment )
• lift( predicate )
• lift( action )
• FIRSTof( goal-structure+ )
• SEQ( goal-structure+ )
• IF( predicate , goal-structure , _goal-structure )
• TRYIF( predicate , goal-structure , _goal-structure )
• WHILE( predicate , goal-structure )
• REPEAT( goal-structure+ )
• DEPLOYonce( agent , GoalFunction ) – Note: a goal function is a function that evaluates the current agent state and constructs a goal.
• DEPLOY( agent , GoalFunction )

The syntax for assigning a goal structure to an agent:

• agent.setGoal( goal-structure )

An agent can also dynamically add and remove goals in its goal-structure (the goal-structure that was given to the agent to solve). This using the following actions:

• addAfter(** GoalFunction )
• addBefore(** goal-_GoalFunction )
• agent. remove( goal-structure )

A testing-goal is a special kind of goal. It can only be given to a test-agent (an instance of the class eu.iv4xr.framework.mainConcepts.TestAgent). It is just an ordinary goal, but additionally it allows an ‘invariant’ to be specified. When the goal is solved, this invariant will also be checked if it also holds. If it does not then we have a violation.

The syntax of testing goals:

• testgoal( name , test-agent ).toSolve( predicate ).invariant( verdictfunction ).withTactic( tactic ) : this creates a new test-goal. A test-goal is an ordinary goal enriched with some testing-related feature. In the above this syntax we can specify an invariant/predicate to check when the goal is achieved. The invariant is expressed as a function that evaluates the agent state, and returns a verdict (pass/fail).

verdictfunction ::= assertTrue_( assertion-name , assertion-info , predicate )

• assertTrue_( test-agent , assertion-name , assertion-info , predicate )

  This is actually a test-goal with a trivial ‘true’ as the goal to solve (so it will always be solved), and the asserted predicate as the invariant to check. Effectively, this checks whether the current agent state satisfies the invariant.

Tactic and action

The syntax of tactics and actions is shown below.

tactic ::=

• action.lift()
• ABORT()
• ANYof( tactic+ )
• FIRSTof( tactic+ ) SEQ( tactic+ )

action ::=

• action( name ).do1( function ).on( predicate )
• action( name ).do2( bifunction ).on( query )

A function is a Java-function, which can be formed with a lambda expression. For example (int x) -> x*x constructs a function that returns 2x given an integer x as input. A bi-function is a Java-function that takes two arguments. Similarly, it can be constructed using a lambda-expression.

DSL for expressing LTL specifications/properties

‘LTL’ stands for Linear Temporal Logic. An LTL formula is essentially a sequence predicate. It can be evaluated on a sequence of values to give a judgement whether or not the sequence satisfies the formula. LTL is explained here.