This page contains some examples of IDP files of increasing complexity. Each of them aims at illustrating one or more aspects of the IDP system.

### Table of Contents

- Running IDP: How to run a simple IDP file
- Hello World: The Lua scripting language in IDP
- Arithmetic: A simple FO(·) theory with arithmetic
- Reachability: An inductive definition and the use of XSB
- Map Colouring: A simple coloring problem, illustrating the mx-library
- N-Queens: Modelling the N-Queens problem in IDP
- Minimization: Optimisation in IDP
- Constructed Types: Constuctor symbols (Herbrand interpretations) in IDP
- Constructed Types: The Einstein puzzleIllustration of the use of constructed types for solving the einstein puzzle.
- Options: An explanation about the most important performance-related options
- Stable Semantics How to change the semantics of IDP to stable models instead of well founded.
- Iterated Inductive Definitions, Linear Time Calculus, Invariants, Progression, ...: Illustration of reuse of knowledge in IDP

### Running IDP

In order to run any of the examples below, simply download the latest IDP binaries for your system from our download page, download the example you with to run (each of them has a download link) and run ./idp my_file.

### Hello World

IDP comes with Lua scripting, hence the easiest way to print "Hello World" to your screen is by using the Lua environment:

procedure main(){ //Everything after // is comment /*So is everything between /* and */ */ print("Hello World") }

A little info: a Lua environment is declared by the keyword "procedure", followed by the name and arguments of this particular procedure. Inside it, a procedural algorithm can be written in Lua syntax. When IDP runs a file, it searches for a procedure with the signature "main()", and starts running the content of the file using this procedure.

### Arithmetic

Of course, the goal of IDP is not to distribute the Lua scripting language but to declaritively solve problems. Consider the problem of assigning values in a certain range to constants (C1 and C2) such that C1 is the smallest of that range and C2 the double of C1. This problem can be declaratively specified in IDP as follows:

vocabulary V{ type someIntegers isa int //someIntegers is a subtype of int C1 : someIntegers //one is a constant of type someIntegers C2 : someIntegers //two is a constant of type someIntegers } theory T: V{ C1 = MIN[:someIntegers]. //C1 is the smallest of sort someIntegers C1 + C1 = C2. //C2 is the double of C1 }

In order to solve a concrete problem, we specify an instance (a structure) and we define in the main procedure what inference we want to use. In this case, we want to perform modelexpansion, since we are searching for an assignment to certain symbols that expands the structure S and satisfies T.

structure S:V{ someIntegers = {1..5} //Define the type someIntegers as the range 1..5 } procedure main(){ stdoptions.nbmodels = 0 //tell IDP to search for all models (in the modelexpand inference) allsols = modelexpand(T,S) if #allsols ~= 1 then print("something is terribly wrong") else print(allsols[1]) end }

### Reachability

In this example we show the use of inductive definitions by means of the reachability relation. The reachability relation on a graph is defined in terms of the graph as follows:

{ //If there is an Edge from x to y, then y is reachable from x ! x y: Reachable(x,y) <- Edge(x,y). //If there is some point between x and y and z is reachable from x, and y from z, then y is reachable from x. ! x y: Reachable(x,y) <- ? z: Reachable(x,z) & Reachable(z,y). }

This definition can be used for various purposes, for example for finding a graph that satisfies certain properties:

theory T: V{ //Reachable is defined inductively as follows: { //If there is an Edge from x to y, then y is reachable from x ! x y: Reachable(x,y) <- Edge(x,y). //If there is some point between x and y and z is reachable from x, and y from z, then y is reachable from x. ! x y: Reachable(x,y) <- ? z: Reachable(x,z) & Reachable(z,y). } //The graph must be fully connected... !x y : Reachable(x,y). //...and can have no edges on impossible locations ! x y: Edge(x,y) => ~Impossible(x,y). }

In case you want to find all models of the above theory expanding a partial interpretation S, you can do this as in the previous example, or use the built-in inference from the mx library:

include < mx > //include the mx module to have some extra built-in procedures procedure main(){ //printmodels and allmodels are methods in the mx include that allow us to shorten our code ;-) printmodels(allmodels(T,S)) }

### Map Colouring

A well known example in AI, is the map colouring problem. Given a map with a collection of countries/areas, we want to find to assign a colour to each area, such that two adjacent areas do not have the same colour. To model this problem we need a set of countries and a set of colours. In addition we also need a function that maps a country to a colour and a relation that says that two countries border each other.

vocabulary V{ type Area type Color Border(Area,Area) Coloring(Area):Color }

The only constraint for this problem is that two adjacent countries do not have the same colour.

theory T:V{ //2 adjacent countries can not have the same color !a1[Area] a2[Area]:Border(a1,a2) | Border(a2,a1) =>Coloring(a1)~=Coloring(a2). // using type inference : !a1 a2 :Border(a1,a2) | Border(a2,a1) =>Coloring(a1)~=Coloring(a2). }

In order to solve a concrete problem, we specify an instance (a structure) and we define in the main procedure what inference we want to use. In this case, we want to perform modelexpansion, since we are searching for an assignment to certain symbols that expands the structure S and satisfies T. Our concrete structure is a map of a part of western Europe.

structure S:V{ Area={Belgium; Holland; Germany; Luxembourg; Austria; Swiss;France } Color={Blue;Red;Yellow;Green} Border={ (Belgium,Holland);(Belgium, Germany);(Belgium,Luxembourg);(Belgium,France); (Holland,Germany); (Germany,Luxembourg);(Germany,Austria);(Germany,Swiss);(Germany,France); (Luxembourg,France); (Austria,Swiss); (Swiss,France) } } procedure main(){ stdoptions.nbmodels = 1 //tell IDP to search for just 1 model (in the modelexpand inference) result= modelexpand(T,S)[1] // Modelexpand(T,S) returns a list of all found models (in this

//case it only contains 1 model), and we need the first model in the list print(result) }

### NQueens

The NQueens problem consists of placing n queens on a n x n board in such a way that no queen can attack another, following the rules of chess.

vocabulary V { type index isa int queen(index, index) n : index type diag isa int diag1(index, index) : diag diag2(index, index) : diag } structure S : V { index = {1..4} diag = {1..7} n = 4 } theory T : V { { diag1(x, y) = x - y + n. } { diag2(x, y) = x + y - 1. } !x[index] : ?=1y[index] : queen(x, y). //(1) !y : ?=1x : queen(x, y). //(2) !d : #{x y : queen(x, y) & diag1(x, y) = d} < 2. //(3) !d : #{x y : queen(x, y) & diag2(x, y) = d} < 2. //(4) }

The vocabulary V consists of a two types (diag and index), one constant (n), one predicate (queen), and two functions (diag1 and diag2). The structure S specifies the size of the n x n board and the diag and index types that follow from this. The predicate queen(index, index) represents where the queens are placed on the board. The function diag1(index, index) : diag maps each square on the board to its upper-left-to-lower-right diagonal. The function diag2(index, index) : diag is defined similarly for the lower-left-to-upper-right diagonals.

The definitions for diag1 and diag2 are placed in theory T and are given between "{" and "}". They are a special kind of definition: all symbols that they depend (in this case: the constant n and the functions + and -) on are completely known. This means that the definition can be calculated, which is more efficient.

The theory also specififies the constraints expressing that the placed queens cannot attack each other. The first constraint expresses that there is exactly one queen on each column of the board: for every x of type index (!x[index]), there is exactly one y of type index (?=1y[index]) for which queen(x, y) holds. The quantified variables are typed in this constraint. This typing is optional and has been omitted in the other constraints as IDP can derive types from the information in the vocabulary.

The second constraint expresses that there is exactly one queen on each row of the board.

The third constraint expresses that for each diagonal (!d) there are less than two elements in the set {x y : queen(x, y) & diag1(x, y) = d}; the set of elements (x, y) such that they satisfy queen(x, y) & diag1(x, y) = d. This ensures that there is no more than one queen on each upper-left-to-lower-right diagonal. The fourth constraint expresses the same for the lower-left-to-upper-right diagonals.

procedure main() { /* Important: the option xsb is not present in every installation, in order to obtain * efficient definition evaluation with XSB, you should compile IDP yourself * (as XSB cannot be distributed with dynamically linked binaries */ stdoptions.xsb=true // use XSB to calculate definitions that can be // calculated in advance diags = calculatedefinitions(T,S) // calculate the definitions for symbols diag1 and diag2 // The resulting variable (diags) contains a single structure // in which the defined symbols are two-valued print(diags) // print of the resulting structure to check the two-valuedness for yourself stdoptions.nbmodels=0 // search for all models solutions = modelexpand(T,diags) // solutions is now a (Lua) table with all models // Note that instead of diags, we could also do modelexpand on S, // since the standard modelexpand workflow contains a call to // calculatedefinitions print(#solutions.." models found") // "#" retrieves table size, .. is the lua concatenation for i,sol in ipairs(solutions) do // A for-loop to iterate over all solutions. print("model "..i..":") // ipairs is a builtin Lua procedure which allows you // to loop over the index and table elements of a table print(sol) end }

The above Lua procedure can then be used to retrieve all models and print them. Here we also introduce the calculatedefinitions method that calculates all definitions that are able to be calculated beforehand, such as the definitions for diag1/2 and diag2/2 in this example. These two definitions can be calculated in advance because they each depend on no other predicate that cannot be calculated in advance. We also introduce the option to use XSB to do this calculation. Note that by default, this option is set to *false*.

### Minimization

In this example, we will illustrate a new form of inference. For now, the only operation executed on an FO(.) theory was model expansion: expanding partial models (or structures) to models. The new inference method is minimization: find a model which is smaller er equal to all other models with respect to a certain criterion.

In this example, would like to find a "still life" (http://en.wikipedia.org/wiki/Still_life_(cellular_automaton)) for a certain grid, which contains a maximal amount of living cells. Firstly, we need a vocabulary:

vocabulary voc { type num isa nat lives(num,num) type neighborAmount isa nat nbOfLiveNeighbors(num,num):neighborAmount }

With the type num the possible row- and column indexes of our square grid of cells, lives a predicate stating which cells are alive, type neighborAmount the number of neighbours with a certain property a cell might have (should always range between 0 and 8), and nbOfLiveNeighbors a function to map each cell to the number of living neighbours. Note that we declare both types to be natural numbers, since we want to be able to use them in mathematical functions.

The theory describing a still life:

theory theo: voc { // Declare how many neighbors of a certain cell are alive !x1 y1: nbOfLiveNeighbors(x1,y1) = #{ x2 y2 : (x1 ~= x2 | y1 ~= y2) & abs(y1-y2) < 2 & abs(x1-x2) < 2 & lives(x2,y2) }. // Cells with exactly three living neighbors must live. !x y: nbOfLiveNeighbors(x,y)=3 => lives(x,y). // Each living cell must have two or three living neighbors. !x y: lives(x,y) => 2=< nbOfLiveNeighbors(x,y) =< 3. }

The more advanced constructs in this theory are the function abs(int) which maps an integer to its absolute value, and the counting aggregate, which counts the number of times a certain propositional formula is true for a set of free variables. Noteworthy is also the "=<" symbol, which denotes the arithmetical "less than or equal to". Many a starting IDP programmer mistakenly writes this as "<=", which actually is the reverse implication (e.g. a=>b is equivalent to b<=a).

A possible structure for our problem setting:

structure struc: voc { neighborAmount = {0..8} num = {1..6} }

Here num ranges from 1 to 6, so we're working in a 6 by 6 grid of cells. neighborAmount is correctly interpreted as ranging from 0 neighbours to 8.

Now, as stated earlier, we want to obtain the still life which has a maximal amount of living cells. As such, our minimization criterion becomes the amount of cells that are not alive. IDP takes this criterion as a term with as type nat, int or float:

```
term t: voc {
// This term represents the amount of non-living cells
#{ x y : ~lives(x,y) }
}
```

The only thing left is to use the lua construct "minimize" with arguments a theory, structure and minimization term to obtain the model with the most living cells:

procedure main() { stdoptions.verbosity.solving = 1 print(minimize(theo,struc,t)[1]) }

For some added insight, we set the verbosity of the solver to 1, so that a new user can see the actual minimization occur.

Constructed types

Note that in the previous example, the interpretation of the type neighbourAmounts is always the same for each instance of the problem: even if the size of the grid is 100x100, each cell can only have 0..8 neighbours with a certain property. It would be nice to state this information outside the structure block, which typically captures instance-specific information. Also, many constraints range over cells, which are currently represented by a pair of xy-coordinates. Being able to quantify over these cells without referring to their coordinates would be more elegant. Thirdly, sometimes you want to be able to refer to specific domain elements without the hassle of defining and interpreting constants manually, for instance when there are too many.

These three use cases are covered by constructed types. A constructed type is a type for which the interpretation is declared in the vocabulary by use of the key words "constructed from". It is constructed from a set of constructor functions, which are declared simultaneously with the constructed type. Each constructor function maps every domain element tuple in its domain to a unique domain element in the interpretation of the constructed type. As a result, the interpretation of the constructed type is the union of the images of its constructor functions. Note that constructor functions can be used in a theory, which is particularly useful if a constructor function is a constant, for which its interpretation will be one unique domain element.

Also, it is possible to interpret types in a vocabulary, meaning that the interpretation will be fixed and independent of any structure. This is done by syntax similar to interpreting types in structures.

The following adapted still-life specification one constructed type, and one type interpreted in the vocabulary. As a result, the modelling is more elegant:

vocabulary V { type num isa nat // A constructed type from the constructor function square type Cell constructed from {square(num,num)} lives(Cell) // A numerical type with a fixed interpretation type neighbourAmount ={0..8} isa int nbOfLiveNeighbours(Cell):neighbourAmount Neighbours(Cell,Cell) Xco(Cell):num Yco(Cell):num } theory T:V { // Define the x-coordinates of a Cell { Xco(c)=x <- ?y: c=square(x,y). } // Define the y-coordinates of a Cell { Yco(c)=y <- ?x: c=square(x,y). } // Define the neighbours of a Cell { Neighbours(c1,c2) <- abs(Xco(c1)-Xco(c2))<2 & abs(Yco(c1)-Yco(c2))<2 & c1~=c2. } // Declare how many neighbours of a certain Cell are alive !c: nbOfLiveNeighbours(c) = #{ c2 : lives(c2) & Neighbours(c,c2) }. // Cells with exactly three living neighbours must live. !c: nbOfLiveNeighbours(c)=3 => lives(c). // Each living Cell must have two or three living neighbours. !c: lives(c) => 2=< nbOfLiveNeighbours(c) =< 3. } structure S:V { num = {1..6} } term O:V { // This term represents the amount of non-living Cells #{ c : ~lives(c) } } procedure main() { print(minimize(T,S,O)[1]); // apparently nothing went wrong :) }

### Constructed types 2: The Einstein Puzzle

Another example using constructed types, the well-known Einstein Puzzle, or also known as the Zebra Puzzle (http://en.wikipedia.org/wiki/Zebra_Puzzle).

vocabulary V{ type House constructed from {Red,Green,Blue,Yellow,White} type Owner constructed from {English, Swede, Dane, Norwegian,German} type Beverage constructed from {Tea,Coffee,Milk,Beer,Water} type Pet constructed from {Dog,Bird,Cat,Horse,Fish} type Cigar constructed from {PallMall,Dunhill,Blend,Bluemaster,Prince} type Nb isa int OwnsHouse(Owner):House OwnsPet(Owner):Pet Drinks(Owner):Beverage Smokes(Owner):Cigar Order(House):Nb } theory T:V{ ! h: ?1 o:OwnsHouse(o)=h. ! p: ?1 o:OwnsPet(o)=p. ! b: ?1 o:Drinks(o)=b. ! n: ?1 h:Order(h)=n. ! c: ?1 o:Smokes(o)=c. //The green house is on the left and next to the white house. Order(White)=Order(Green)+1. //The green homeowner drinks coffee. !x:OwnsHouse(x)=Green => Drinks(x)=Coffee. //The person who smokes Pall Mall rears birds. !x:Smokes(x)=PallMall => OwnsPet(x)=Bird. //The owner of the yellow house smokes Dunhill. !x:OwnsHouse(x)=Yellow => Smokes(x)=Dunhill. //The man living in the center house drinks milk. !h x:OwnsHouse(x)=h & Order(h)=3 => Drinks(x)=Milk. //The Norwegian lives in the first house. !h: OwnsHouse(Norwegian)=h => Order(h)=1. //The man who smokes Blends lives next to the one who keeps cats. !x1 x2 h1 h2: OwnsHouse(x1)=h1 & OwnsHouse(x2)=h2 & Smokes(x1)=Blend &OwnsPet(x2)=Cat => (Order(h1)=Order(h2)+1 | Order(h1)=Order(h2)-1). //The man who keeps the horse lives next to the man who smokes Dunhill. !x1 x2 h1 h2: OwnsHouse(x1)=h1 & OwnsHouse(x2)=h2 & OwnsPet(x1)=Horse &Smokes(x2)=Dunhill => (Order(h1)=Order(h2)+1 | Order(h1)=Order(h2)-1). //The owner who smokes Bluemaster drinks beer. !x : Smokes(x)=Bluemaster => Drinks(x)=Beer. //The German smokes Prince. Smokes(German)=Prince. //The Norwegian lives next to the blue house. !h: OwnsHouse(Norwegian)=h => (Order(h)=Order(Blue)+1 | Order(h)=Order(Blue)-1). //The man who smokes Blends has a neighbor who drinks water. !x1 h1 : OwnsHouse(x1)=h1 & Smokes(x1)=Blend => ?x2 h2:( OwnsHouse(x2)=h2 &(Order(h1)=Order(h2)+1 | Order(h1)=Order(h2)-1) & Drinks(x2)=Water). } structure S:V{ Nb={1..5} // Hints // The Englishman lives in the red house. OwnsHouse < ct> = {English->Red} // The Swede keeps dogs as pets. OwnsPet < ct> = {Swede->Dog} // The Dane drinks tea. Drinks < ct> = {Dane->Tea} } include < mx> procedure main() { printmodels(allmodels(T,S)) }

### Options

IDP has several useful options. For example, default, IDP performs model expansion by ground and solve: first grounding the input to a propositional theory and subsequently calling an (extended) SAT solver. When domains are very large, the grounding often becomes unfeasible. For example, translating the following theory to SAT quickly consumes all memory in an average computer if A, B and C range over a large domain.

theory T:V{ A+B=C. A+3*B>C-5*A. }

In the field of constraint programming, large domains are often not a problem. Therefore, the SAT solver (minisatID) underlying IDP has been extended with constraint programming modules. The CP solver can be activated with:

stdoptions.cpsupport=true

Other techniques for avoiding too large grounding are:

- using XSB to calculate definitions of which all opens are known:
stdoptions.xsb=true

- lazy grounding (interweaving ground and solve)
stdoptions.tseitindelay=true stdoptions.satdelay=true

Furthermore, before starting the grounding process, by default IDP performs an approximation step in order to try to reduce groundingsize. This step can be disabled by:

stdoptions.groundwithbounds=false stdoptions.liftedunitpropagation=false

Another useful options influencing performance is symmetry breaking. Often, domain elements are interchangeable (for example pigeons in the pigeon hole problem, nurses in rostering problems, ...). Automated symmetry breaking methods can be enabled with

stdoptions.symmetrybreaking="static"

### Stable Semantics

In normal circumstances, IDP uses well-founded semantics. However, sometimes the user is interested in models according to the stable model semantics. IDP can handle this through the use of the stablesemantics option.

```
vocabulary V {
p
q
}
theory T : V {
{
p <- ~q.
q <- ~p.
}
}
structure S : V{
}
include < mx>
procedure main(){
//declares that IDP uses stable semantics instead of well-founded semantics from this point on
stdoptions.stablesemantics = true
printmodels(allmodels(T,S))
}
```

### Iterated Inductive Definitions, Linear Time Calculus, Invariants, Progression, ...

Iterated inductive definitions are a well-known fenomenon in mathematics. An iterated inductive definition consists of a sequence of inductive definitions. Each of the definitions can refer (both positively and negatively) to stuff defined in earlier (in the sequence) definitions. In order to find the model of such an iterated inductive definition, you should calculate the models of each of the smaller definitions in the specified order. It has been shown that you can throw all of the separate definitions in one big definitions and that the well-founded semantics still formalises the iterated induction correctly.

Itereated inductions occur in real-world problems too. Consider for example a variant of the well-known blocks world planning domain. Given is a set of blocks on a table. A robot can execute action pickup to pick up a block and action put to put the block on the table or another block. When a block is picked up on top of which other blocks are piled up, the effect of this action depends on the size of the pile: if the size exceeds a given threshold, then the pile collapses and all blocks fall on the table with exception of the picked one. Otherwise, the robot can hold and move the block and all blocks piled on it. We assume that initially the robot’s hand is empty. We formalise this in the example below.

In this example, we will also demonstrate the Linear Time Calculus, how the induction method can be used to prove invariants about a theory over time, and how the progression inverence can be used for interactive simulation.

/* The header LTCvocabulary is only supported in IDP 3.2.2 and above. In older versions, you can use vocabulary instead*/ LTCvocabulary V{ //These three are standard in planning problems: Time, an initial time and a successor function //The header "LTCvocabulary" indicates among others that these three constructs will be present and what their meaning is. type Time isa nat Start: Time partial Next(Time):Time //The successor is partial since we will search for plans in a finite context. In that case, the last state has no successor anymore. //The objects in our world consist of blocks and one Table type Object Table:Object //The fluents contain info on the location of the Objects (on eachother or on the table or in the hands of the robot) On(Time, Object, Object) //first object is on second Holds(Time, Object) //This predicate describes the initial situation I_On(Object, Object) //One derived fluent: Above: whether one Object is above another Above(Time, Object, Object) //first object is above second //Another derived fluent: Falls: true when a block is caused to fall. Falls(Time, Object) //The actions: a robot can take or put down Take(Time, Object) Put(Time, Object, Object) //Put the first object on the second //MaxBlocks determines the maximum number of blocks a robot can hold. E.g., if MaxBlocks = 2, a robot can hold a block with one on top. type numbers isa int MaxBlocks: numbers } theory T:V{ //Check if the initial situation is a valid one: the table cannot be on other blocks ! b: ~ I_On(Table,b). //In fact, the above should hold at any point in time; it should be an invariant of the theory. We shall check this later on. //A robot can only take one action at a time !t : #{b: Take(t,b)} + #{b b': Put(t,b,b')} < 2. //Preconditions: // * A robot can only put things down that he has ! t b: (?b': Put(t,b, b' )) => Holds(t,b). // * A robot can never take the table ! t: ~Take(t, Table). // * A robot cannot take something if he is holding something else ! t b: Take(t,b) => ~ ?b': Holds(t,b') . // * A robot cannot put a block on an occupied block ! t b b': Put(t,b,b') & b' ~= Table => ~ ? b2: On(t,b2,b'). // * A robot can only put a block on a block that is resting (indirectly) on the table ! t b b2: Put(t,b,b2) => Above(t,b2,Table). { //Above is the transitive closure of On for every point in time. !t b1 b2: Above(t, b1, b2) <- On(t, b1, b2). !t b1 b2: Above(t, b1, b2) <- ? b3: On(t, b1, b3) & Above(t,b3,b2). //A block falls if the robot tries to take a too high pile. ! t bF: Falls(t,bF) <- ? bT: Take(t,bT) & Above(t, bF,bT) & #{bS: Above(t, bS, bT)} + 1 > MaxBlocks . //A robot holds a block if he takes it ! t b: Holds(Next(t),b) <- Take(t,b). //Or if he had it and does not put it away. ! t b: Holds(Next(t),b) <- Holds(t,b) & ~ ? b': Put(t,b,b'). //An object is on another object if: // * Initially: given by I_On ! b1 b2: On(Start, b1, b2) <- I_On(b1,b2). // * Someone puts it there ! t b1 b2: On(Next(t), b1, b2) <- Put(t, b1, b2). // * it was already there and // * - It is not moved AND // * - there is no block lower in the stack that is picked up and causes this blocks to fall ! t b1 b2: On(Next(t), b1, b2) <- On(t, b1, b2) & ~ Take(t, b1) & ~ Falls(t,b1). // * In case a block falls, he ends up on the table ! t b: On(Next(t), b, Table) <- Falls(t,b). } } structure S:V{ Time = {0..4} Object = {B1;B2;B3;T} Table = T I_On={B1,T;B2,B1;B3,B2} MaxBlocks=2 } //We expect that these are invariants of the theory //Note: sometimes it is enough to put few invariants here. //Proving invariants with the induction method sometimes require that they are strong enough. //That is why we put them all in one theory. theory invariant:V{ //The table is never on something else !t : ~ ? b: On(t, Table,b). //No block is ever on itself ! t b: ~On(t,b,b). //No block is ever above itself ! t b: ~Above(t,b,b). //Two blocks can never rest on the same block. ! t b : b ~= Table => #{b': On(t, b',b)} < 2. //A block can only rest on one block at most. ! t b : #{b': On(t, b, b')} < 2. //The robot can never hold the table !t : ~Holds(t, Table). //The robot can hold at most one block !t : #{b:Holds(t, b)} < 2. //A block cannot both be on another block and in the hands of the robot ! t b: Holds(t,b) => ~?b2: On(t,b,b2). } //This theory simply tells how to interpret Start and Next theory TimeTheo : V{ { Start = MIN[:Time]. !t : Next(t) = t + 1 <- Time(t+1). //Next is incrementing as long as this stays within bounds } } //This theory can contain possible goals of a planning problem theory goal : V{ //All blocks are on the table after at most two actions ? t: t<3 & ! b: b~= Table => On(t,b,Table). } include < mx > procedure main(){ //first we fix the interpretation of Start and Next //the calculatedefinitions procedure returns a partial structure that equal S except on defined symbols in TimeTheo: for every definition in TimeTheo such that it's unique model //can already be calculated (i.e., the opens are known in S) it calculates that unique model. S = calculatedefinitions(TimeTheo,S) //We can simply compute models of this theory: print("----> This is a model of T:") print(modelexpand(T,S)[1]) //We can check invariants on this theory /* invariant checking is only supported in IDP 3.2.2 and above.*/ if isinvariant(T,invariant, S) then print("----> Okay, we proved --using the induction method-- that in this given context, our invariant is satisfied") else print("----> Something is wrong with our theory") end //We can do planning on this theory //planningtheo consists of the union of everything in T and everything in goal local planningtheo = merge(T, goal) print("----> This is a model of T such that goal is reached") print(modelexpand(planningtheo, S)[1]) //We can calculate 10 possible initial states... stdoptions.nbmodels = 10 /* initialise and progress are only supported in IDP 3.2.1 and above.*/ print("----> Starting interactive simulation") local states = initialise(T,S) //...and use one of those initial states to continue with (again and again and ...) while true do printmodels(states) print("Please enter which state to use") local num = tonumber(io.read("*line")) local chosen = states[num] states = progress(T,chosen) end }