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.  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.