Impressum planner.vdmsl Sprache: VDM

\begin{vdm_al}
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}

\end{vdm_al}

quality89%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.