Overture Tool

              
types

	Literal = seq of token; 
	State = set of Literal;
	Goal = set of Literal;
	Action :: name : Literal
		pra	 : set of Literal
		add	 : set of Literal
		del	 : set of Literal;
	
	Planning_Problem :: AS : set of Action
		          I : State
		          G : Goal

	inv  mk_Planning_Problem ( AS, I, G) ==
	forall l in set G &
		 (l in set I or 
		exists A in set AS & l in set
		 A.add)
	and 		   			                         
	not (G subset I) and
	forall A in set AS & not (exists p : Literal & p in set A.add and
		p in set A.del); 

Action_id = token;
Action_instances = map Action_id to Action;

Arc ::
	  source	: Action_id
          dest    	: Action_id;

Bounded_Poset = set of Arc
inv  p ==
	forall x, y in set get_nodes(p) & 
	not (before(x, y, p) and before(y, x, p)) and
	x <> mk_token("pinit") => before(mk_token("pinit"), x, p) and 
	x <> mk_token("goal") => before(x, mk_token("goal"), p);

 Goal_instance :: 
		   gl : Literal
		   ai : Action_id;

Goal_instances = set of Goal_instance

state Partial_Plan of
	pp: Planning_Problem
	Os: Action_instances
	Ts: Bounded_Poset
	Ps: Goal_instances
	As: Goal_instances
inv  mk_Partial_Plan(pp, Os, Ts, Ps, As)== 
	(Os(mk_token("pinit")) = mk_Action([mk_token("pinit")], { }, pp.I, { })) and
	(Os(mk_token("goal")) = mk_Action([mk_token("goal")], pp.G, { }, { })) and
	rng Os subset pp.AS union {Os(mk_token("pinit")), Os(mk_token("goal"))} and
	dom Os = get_nodes(Ts) and
	As inter Ps = {} and
	forall A in set dom Os & (forall p in set Os(A).pra &  
       		mk_Goal_instance(p, A) in set (Ps union As)) and
	forall gi in set As & exists A in set dom Os & achieve(Os, Ts, A, gi)
end

functions

get_nodes : set of Arc -> set of Action_id
get_nodes(p) ==
	{a.source | a in set p} union {a.dest | a in set p};

before : Action_id * Action_id * set of Arc -> bool 
before(x, z, p) ==
	mk_Arc(x, z) in set p or
	exists y in set get_nodes(p) & before(x, y, p) and before(y, z, p);

possibly_before : Action_id * Action_id * set of Arc -> bool 
possibly_before(x, z, p) ==
	x <> z and not before(z, x, p);

completion_of : Bounded_Poset * Bounded_Poset -> bool 
completion_of(p, q) ==
	(forall x, y in set get_nodes(p) & before(x, y, q) and before(x, y, p));

initposet: () -> Bounded_Poset
initposet() ==
	{mk_Arc(mk_token("pinit"), mk_token("goal"))};

add_node : Action_id * Bounded_Poset -> Bounded_Poset
add_node(u, p) ==
	p union {mk_Arc(mk_token("pinit"), u), mk_Arc(u, mk_token("goal"))};

make_before : Action_id * Action_id * Bounded_Poset -> Bounded_Poset
make_before(u, v, p) ==
	if possibly_before(u, v, p) and {u, v} subset get_nodes(p)
	then p union {mk_Arc(u, v)} else p;


newid(isa : set of Action_id) i: Action_id 
post i not in set isa;

achieve : Action_instances * Bounded_Poset * Action_id * Goal_instance -> bool 
achieve(Os, Ts, A, mk_Goal_instance(p, O)) ==
	before(A, O, Ts) and
	p in set Os(A).add and
	not (exists C in set dom Os & 
	possibly_before(C, O, Ts) and 
	possibly_before(A, C, Ts) and
	p in set Os(C).del); 

declobber:Action_instances * Bounded_Poset * Action_id * Goal_instance -> bool 
declobber(Os, Ts, NewA, mk_Goal_instance(q, C)) ==
	before(C, NewA, Ts) or
 	not(q in set Os(NewA).del) or
	exists W in set dom Os & 
	(before(NewA, W, Ts) and
	before(W, C, Ts) and
	q in set Os(W).add)

operations

INIT (ppi : Planning_Problem)
ext	wr pp : Planning_Problem
	wr Os : Action_instances
	wr Ts : Bounded_Poset
	wr Ps : Goal_instances
	wr As : Goal_instances
post	pp = ppi and
	Os =  {mk_token("pinit") |->  mk_Action([mk_token("pinit")], { }, 
			ppi.I, { }), 
			 mk_token("goal") |->
				 mk_Action([mk_token ("goal")], ppi.G, { }, { })} and
	Ts = initposet( ) and
	Ps = {mk_Goal_instance(g, mk_token("goal")) | g in set ppi.G} and
	As = { };


ACHIEVE_1(gi : Goal_instance)
ext	rd Os : Action_instances
	wr Ts : Bounded_Poset
	wr Ps : Goal_instances
	wr As : Goal_instances
pre	gi in set Ps
post	exists A in set dom Os & achieve(Os, Ts, A, gi) and
	completion_of (Ts, Ts~) and 
	Ps = Ps~ \{gi} and 
	As = As~ union {gi};


ACHIEVE_2(gi: Goal_instance)
ext	rd pp : Planning_Problem
	wr Os : Action_instances
	wr Ts : Bounded_Poset
	wr Ps : Goal_instances
	wr As : Goal_instances
pre	gi in set Ps
post	let NewA = newid(dom Os~) in
	exists A in set pp.AS & Os = Os~ ++ {NewA |-> A} and
	achieve(Os, Ts, NewA, gi) and
	forall gj in set As~ & declobber(Os, Ts, NewA, gj) and
	completion_of(Ts, add_node(NewA, Ts~)) and 
	Ps = (Ps~ \ {gi}) union {mk_Goal_instance(p, NewA) | p in set A.pra} and
	As = As~ union {gi}