The PMON system
This is a quick guide to the PMON system. The documentation is far
from complete (since I had to write it in a hurry), but hopefully it will
be sufficient for the exercise.
If you have any questions or comments, feel free to contact me:
jonkv@ida.liu.se .
PMON can be run either as an applet under Netscape, MS Explorer or other browsers: http://www.ida.liu.se/~jonkv/PMON.html, or as an application run from a shell.
In the former case, you cannot load or save files on your own machine
(due to the safety restrictions built into Java).
In the latter case, you first need to select the WWW module.
module add misc/www
Then you can start the application as follows:
~aik/pmon/startpmon
Using the PMON tool
This section contains a very brief introduction to using the tool.
Writing scenario descriptions
Scenario descriptions are written in the topmost text area. In the text
area at the bottom, you can see different translation of the scenario;
you will probably not need to use this, but if you want to, you can switch
between different translations using the choice box between the
text areas. The update button updates the translation when you have
made changes to the scenario description.
The editing capabilities of the text area are not very good; if you want
to, you can write your scenario description in Emacs, load it into the
tool using the "Open scenario description" menu item, and then
reload it with the reload button whenever you have made changes.
Showing the models of the scenario description
If you press "Show initial", you will get an initial approximation
of the models of the scenario description. If you press "Show
models", you will see all models of the scenario description.
Models are shown using one timeline for each boolean fluent and one timeline
per value for each non-boolean fluent.
For boolean fluents, green means that the fluent is true at the timepoint
in the model, red means that the fluent is false, and gray means
that the fluent can be either true or false.
For non-boolean fluents, green means that the fluent can have that
value at the timepoint, and red means that the fluent can not have
that value at the timepoint.
White means that the fluent must have the same value as it had the
previous timepoint. (This may sound complicated, but will probably
be more easily understood once you look at the actual timelines.)
Querying the system
To query the system, press "Show models" and then select
"Query" from the menu. This will give you a new window
with a text field where you can enter your query. A query is a logic
formula, such as "[100] broken == false". When
you press the "Evaluate query" button, you will get an answer
telling you the number of models in which this formula is true, false,
or unknown.
-
If there are only models in which the formula is true, the formula
follows from the scenario.
-
If there are only models in which the formula is false, the negation
of the formula follows from the scenario.
-
If there are both models in which the formula is false and models in
which the formula is true, neither the formula nor its negation follows
from the scenario.
-
If there are models in which the formula is unknown, you don't know
whether the formula or its negation follows from the scenario; this is
because the query algorithm is currently not complete.
For example, if you get the answer "0 true, 12 false, 0 unknown",
you know that the formula is false in all models; if you get the answer
"0 true, 10 false, 2 unknown", you don't know whether the formula
is false in all models or not, since the formula is unknown in two models.
Examples
There are several example scenario descriptions in the "Examples"
menu in the main window. To see an example, select it from the menu.
Note that this will overwrite any scenario you have written in the text
area, so make sure that you have saved your work. One of the
examples is the following (the Russian Turkey Scenario):
//
// Russian Turkey Scenario
//
feature alive boolean, loaded boolean
action Load, Fire, Spin
obs [0] alive & !loaded
occ [1,2] Load
occ [3,4] Spin
occ [5,6] Fire
acs [t1,t2] Load ~> [t1,t2] loaded := T
acs [t1,t2] Spin ~> [t1,t2] loaded := TF
acs [t1,t2] Fire ~> [t1] loaded -> [t1,t2] alive := F & loaded := F
The language of scenario descriptions
In order to define scenario descriptions, you must first declare the features/fluents,
value domains and action symbols that you want to use. After all
declarations, you add action law schemas, observation statements, and action
occurrences.
Value domains
A value domain is defined using the syntax
domain <name> = { <value1>, <value2>, ..., <valuen> }
For example, you could define a domain containing fruit:
domain fruit = { apple, orange, banana }
There is one predefined value domain, boolean, which contains
the two values true and false.
Features
A feature can take zero or more values from value domains as arguments.
It is defined using the syntax
feature <name> <value domain>
or
feature <name>(<argument domain 1>, ..., <argument domain n>)
<value domain>
For example, assume that you have defined a domain car containing
cars, and want a feature that is true iff a given car is broken:
feature broken(car) boolean
On the other hand, if you are only reasoning about one car, you may never
mention it explicitly. Instead, you could have a feature without
arguments:
feature car_is_broken boolean
Assume that you have defined a domain locations containing different
places, and that you have defined a domain people containing people.
You want to know where the people are. You could do this in one of
two ways:
feature place_of(people) location
feature is_at(people, location) boolean
The second way would allow someone to be at several locations, or at no
location at all. If this is not what you intended, you may need to
use domain constraints to enforce the condition that everyone is always
at exactly one place.
Action symbols
You must declare an action symbol for each action that you want to define.
The syntax for this, with or without arguments, is:
action <symbol>
action <symbol>(<argument domain 1>, ..., <argument domain n>)
For example, in the broken car example above, you may want an action that
breaks a car:
action break(car)
You may want an action that moves someone to a location:
action move(people, location)
Action law schemas
An action law schema defines the actual meaning of an action symbol:
acs [t1,t2] move(v[people], v[location]) ~>
[t1] !(place_of(v[people]) == v[location]) ->
[t1,t2] place_of(v[people]) := v[location]
An action is executed during a time interval. The schema above defines
what happens when an action is executed during the time interval [t1,t2],
where t1 and t2 are temporal variables.
The action that is defined is the move action. It takes
two arguments. In the action symbol definition, we used the names
of the value domains, people and location. Now, we must use value
variables instead; when we actually execute the action, these value
variables will be replaced by the actual arguments of the action occurrence
statement (to be defined below). Value variables are named (a bit
awkwardly) v[domainname], v0[domainname], v1[domainname],
and so on.
The "~>" symbol consists of a tilde followed by a "larger
than" sign, and separates the action symbol with arguments from the
actual reassignment formula.
The reassignment formula can be conditional, which it is in this case:
We have a precondition saying that we don't execute the action if the given
person is already in the given location. Here, the "=="
symbol (double equality signs) are the equivalent of "equals with
a hat" in Features and Fluents; we only execute the action if
at time t1, it is not the case that the place of the person belongs to
the set consisting of the v[location] argument. As in Features
and Fluents, we can use either a single value, such as v[location], or
a set of values, such as {here, there, v[location]}.
The precondition can be an arbitrary fluent formula -- in this exercise,
an arbitrary boolean combination of "fluent == value" comparisons,
where the boolean operators are the following (using the standard
precedence rules):
<->
|
Equivalence
|
->
|
Implication
|
|
|
Disjunction
|
&
|
Conjunction
|
!
|
Negation
|
Finally, if the condition is true, then during the interval [t1,t2], the
feature place_of(v[people]) gets the new value v[location].
This is done using the reassignment operator ":=" (colon-equals).
An action law schema can change several fluents using the "&"
operator, and can contain alternatives using the "|" operator:
acs [t1,t2] whatever ~> [t1,t2] something1 := true & something2 := false |
something1 := false & something2 := true
Here, both something1 and something2 will get new values. When the
action has been executed, either something1 == true & something2
== false or something1 == false & something2 == true.
Action occurrence statements
Action occurrence statements define which actions are executed when.
The syntax is:
occ [<time1>,<time2>] <action symbol>
or
occ [<time1>,<time2>] <action symbol>(<arguments>)
For example:
occ [5,7] move(me, there)
Observation statements
An observation statement consists of a logic formula that must be true
in any model of the scenario description. For example, you can specify
the state at time zero:
obs [0] place_of(me) == here & place_of(you) == there
obs [0] forall v[car] [ !broken(v[car]) ]
You can use all of the boolean operators defined in the table above.