Specification
|
Specification
For this benchmark version, seven hypothesis are considered.
- Each repository stores only one particular type of raw material
- A repository has exactly one connection port to machines (i.e., it is able to supply at most one machine at a time).
- Repositories have an unlimited supply of raw material.
- Machines have two ports, but need exactly two different raw materials to generate a product.
- If a machine is not clean, it can non-deterministically break when trying to generate certain products.
- Just before producing, a repository must have its valve opened to supply the products to a machine. A valve can only be opened if a connection was established to a machine.
- Temporal specifications are defined in Linear Temporal Logic (LTL).
With this in mind, the following literals are defined to represent a problem state.
| connectedCIMJ |
iff repository I is connected to machine J |
| haveRawProductRIMJ |
iff machine J has raw product from repository I |
| freePortCI |
iff the port of repository I is free |
| bothPortsFreeMI |
iff machine I has both ports free |
| onePortFreeMI |
iff machine I has only one port free |
| noPortFreeMI |
iff machine I has no ports free |
| notCleanMI |
iff machine I is not clean |
| breakMI |
iff machine I has broken |
| generatedPIPJ |
iff product from materials in repositories I and J were generated |
| notGeneratedPIPJ |
iff product from materials in repositories I and J were not generated (red.) |
| readyToOpenValveCI |
iff repository I may open its valve |
| valveOpenCI |
iff repository I has its valve already opened |
Both controllable actions and uncontrollable events are defined using STRIPS representation, where each action (event) has a set of preconditions (pre), a set of positive effects (add) and a set of negative effects (del). They are described in the next two sections.
Controllable Actions
The controllable actions are:
| action_connect1_CI_MJ |
| pre: |
freePortCI, bothPortsFreeMJ |
| add: |
connectedCIMJ, onePortFreeMJ |
| del: |
freePortCI, bothPortsFreeMJ |
| Connects repository I and machine J, considering that machine J has the other port free. |
| action_connect2_CI_MJ |
| pre: |
freePortCI, onePortFreeMJ |
| add: |
connectedCIMJ, noPortFreeMJ |
| del: |
freePortCI, onePortFreeMJ |
| Connects repository I and machine J, considering that machine J has no ports free. |
| action_disconnect1_CI_MJ |
| pre: |
connectedCIMJ, onePortFreeMJ |
| add: |
freePortCI, bothPortsFreeMJ |
| del: |
connectedCIMJ, onePortFreeMJ |
| Disconnects repository I and machine J, considering that machine J has the other port free. |
| action_disconnect2_CI_MJ |
| pre: |
connectedCIMJ, noPortFreeMJ |
| add: |
freePortCI, onePortFreeMJ |
| del: |
connectedCIMJ, noPortFreeMJ |
| Disconnects repository I and machine J, considering that machine J has no ports free. |
| action_clean_MI |
| pre: |
notCleanMI |
| add: |
- |
| del: |
notCleanMI |
| Cleans machine I. |
Uncontrollable Events
The uncontrollable events are:
| event_generate_productRIRJMK |
| pre: |
haveRawProductRIMK, haveRawProductRJMK, notGeneratedPIPJ |
| add: |
generateProductPIPJ |
| del: |
haveRawProductRIMK, haveRawProductRJMK, notGeneratedPIPJ |
| Generation product in machine K using materials from repositories I and J. |
| event_break_RIRJMK |
| pre: |
haveRawProductRIMK, haveRawProductRJMK, notCleanMK |
| add: |
breakMK |
| del: |
- |
| Breaking of machine K due to generation of a product while K was not clean. |
| event_transaction_CIMJ |
| pre: |
connectedCIMJ, valveOpenCI |
| add: |
haveRawProductRIMJ |
| del: |
valveOpenCI |
| Raw material transaction from repository I to machine J. |
| event_set_ready_to_open_CIMJ |
| pre: |
connectedCIMJ, haveRawProductRIMJ,
onePortFreeMJ |
| add: |
readyToOpenValveCI |
| del: |
- |
| Preparation to open valve from repository I. |
| event_consume_product_PIPJ |
| pre: |
generatedPIPJ |
| add: |
notGeneratedPIPJ, readyToOpenValveCI, readyToOpenValveCJ |
| del: |
generatedPIPJ |
| Consumption of product from raw materials in repositories I and J. |
| event_close_valve_CI |
| pre: |
valveOpenCI, freePortCI |
| add: |
readyToOpenValveCI |
| del: |
valveOpenI |
| Close valve from repository I. |
| event_open_all_valves |
| pre: |
readyToOpenValveC... |
| add: |
valveOpenC... |
| del: |
readyToOpenValveC... |
| Open valves from all repositories. |
LTL Formulae
Two types of formulae are considered in this version. Firstly, no machines should ever break, G(!breakMI). Secondly, some products must be eventually generated, F(generatedPIPJ).
Back to the beginning.
|