# DTAI

KRR Software: IDP examples

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.

### 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
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 and Aggregates

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. Next to this, we will also introduce a new language construct: aggregates. Aggregates are used in IDP to express properties of sets. Using this language construct it is possible to express the cardinality of a set or the minimum, maximum, sum or product of the elements in that set.

To illustrate this new inference and new language construct, we will look at different version of a shortest path problem in this example.

#### Shortest path example 1

The first version is the simplest version where a number of nodes (roads in this specific example) and edges (roads) are given. The following vocabulary is used;

```vocabulary V{
type city
Path(city,city)
Start:city
End:city
Reaches(city,city)
}
```

Next to the given roads and cities, this vocabulary also contains a startnode, an endnode, paths (the roads taken by the shortest path) and a reachability relation. The theory describing this shortest path problem:

```theory T:V{
Reaches(Start,End).
{
!x y:Reaches(x,y)← Path(x,y) | Path(y,x).
!x y:Reaches(x,y)← ?z: Reaches(x,z) & Reaches(z,y).
}
}```

It contains a constraint that only existing roads can be used and that the shortest path must go from Start to End. It also defines the reachability relation. The input information is given using a structure and consists of a set of cities and the existing roads between them:

```structure S:V{
city= {Reno; Chicago; Fargo; Minnesota; Buffalo; Toronto; Winslow; Sarasota;
Wichita; Tulsa; Ottawa; Oklahoma; Tampa; Panama; Mattawa}
(Tampa,Oklahoma);(Panama,Mattawa);(Panama,Tampa);(Oklahoma,Tulsa);(Ottawa,Minnesota);(Tulsa,Buffalo);(Buffalo,Tulsa)}
Start=Reno
End=Mattawa
}```

The express the minimality we will use the cardinality aggregate together with the new minimisation inference. We want to minimize the number of roads that are used in the shortest path. To do this, we construct the following term which represents the number of roads taken:

```term O:V{
#{x,y:Path(x,y)}
}```

With all this information, the following simple procedure will print a shortest path solution:

```procedure main(){
result= minimize(T,S,O)[1]
print(result)
}
```

#### Shortest path 2

To show another example of using a set expression in IDP, we will extend previous example with weights. The roads will now have a distance, so to determine the shortest distance,the sum of all distances has to be calculated instead of the number of used roads. This is the IDP specification of the new version:

```vocabulary V{
type city
type distance isa int
partial Path(city,city):distance
Start:city
End:city
Reaches(city,city)
}
theory T:V{
Reaches(Start,End).
{
!x y:Reaches(x,y)<- ?d:Path(x,y)=d | Path(y,x)=d.
!x y:Reaches(x,y)<- ?z: Reaches(x,z) & Reaches(z,y).
}
}
structure S:V{
city= {Reno; Chicago; Fargo; Minnesota; Buffalo; Toronto; Winslow; Sarasota;
Wichita; Tulsa; Ottawa; Oklahoma; Tampa; Panama; Mattawa}
(Tampa,Oklahoma,2);(Panama,Mattawa,1);(Panama,Tampa,11);(Oklahoma,Tulsa,17);(Ottawa,Minnesota,3);(Tulsa,Buffalo,4);(Buffalo,Tulsa,10)}
Start=Reno
End=Mattawa
}
term O:V{
sum{x,y,d:Path(x,y)=d:d}
}
procedure main(){
result= minimize(T,S,O)[1]
print(result)
}```

### Aggregates 2

Next to the sum and cardinality, IDP also supports the minimum, maximum and product of the elements in a set. Here we will demonstrate the product aggregate, by using a simple prime decomposition example.

### Minimization 2

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:

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 chosen = states[num]
states = progress(T,chosen)
end
}
```

### Concrete Delivery: an OR problem solved with IDP

This project was made to test whether IDP was able to model a typical OR problem reasonably well. The problem at hand was the concrete delivery problem, which consisted of finding a configuration of truck trips that delivered concrete to customers during a restricted timeframe. More information can be found in the report.

```vocabulary V{
// Given:
type Truck
type Site
type Customer isa Site
Start:Site
End:Site
type Amount isa int
Request(Customer):Amount
TotalRequest:int
type ExtendedTime isa int
type Time isa int
WindowStart(Customer):Time
WindowEnd(Customer):Time
TravelTime(Site,Site):Time
type Cap isa int
Capacity(Truck):Cap
MaxTimeLag:int
type Trip isa int
UpperBound(Truck):Trip

// Find:
Satisfied(Customer)

// Actions:
Destination(Truck,Trip):Site
Arrival(Truck,Trip):Time

// Properties:
FinalTrip(Truck):Trip
ConcreteDelivered(Customer):Amount

// Tseitins:
RealTrip(Truck,Trip)
Follows(Truck,Trip,Truck,Trip)
Last(Truck,Trip)
}

Term Satisfieds:V{
sum{c:~Satisfied(c):Request(c)}
}

theory T:V{
// Defining the amount of concrete delivered to a customer
!c[Customer]: ConcreteDelivered(c) = sum{trk trip : c=Destination(trk,trip) : Capacity(trk)}.

// Definition of a satisfied customer
!c[Customer]: Satisfied(c) <=> ConcreteDelivered(c)>=Request(c).

// Define tseitins:
!trk trip: RealTrip(trk,trip) <=> Customer(Destination(trk,trip)).
!trk trip trk2 trip2: Follows(trk,trip,trk2,trip2) <=> Destination(trk,trip)=Destination(trk2,trip2) & Arrival(trk,trip)= RealTrip(trk,trip) & ~? trk2 trip2: Follows(trk,trip,trk2,trip2).

// Starting at the start point at time 0.
!trk: Arrival(trk,0)=0.
!trk: Destination(trk,0)=Start.
!trk trip[Trip]: trip>0 => Destination(trk,trip)~=Start.
// Going to customers between start and end
!trk trip: RealTrip(trk,trip) <=> trip>0 & trip= FinalTrip(trk) => Destination(trk,trip)=End & Arrival(trk,trip)=MAX[:Time].
// Use upper bound (some extra constraints to help grounder)
!trk trip[Trip]: trip >= UpperBound(trk) => Destination(trk,trip)=End & Arrival(trk,trip)=MAX[:Time].

// Deliveries must happen in the desired time windows
!trk trip[Trip]: RealTrip(trk,trip) => WindowStart(Destination(trk,trip))= WindowEnd(Destination(trk,trip))>=Arrival(trk,trip)+UnloadTime(trk).

// When one truck is unloading at a site, another truck can't arrive
// (we assume the second truck should wait a little before arriving, because we assume arriving is starting unloading)
!trk trip[Trip]: RealTrip(trk,trip) => ~? trk2 trip2: Follows(trk,trip,trk2,trip2) & Arrival(trk2,trip2) (? trk2 trip2: Follows(trk,trip,trk2,trip2) & Arrival(trk2,trip2)= Satisfied(Destination(trk,trip)).
! trk trip: RealTrip(trk,trip) <=> 0 ConcreteDelivered(c)=0 & ! trk trip: Destination(trk,trip)~=c.
! c[Customer] trk trip: (Destination(trk,trip)=c & Last(trk,trip)) => Request(c)+Capacity(trk) > ConcreteDelivered(c).
}
```

### Modeling sensitive information flow with IDP3

This project constructs a framework to reason about privacy properties based on given trust relationships in the context of complex electronic services. This paper offers a description of the model, as well as explains some of the design choices that were made. The theory and an example instance are given below. More information, as well as additional instances, can be found on the project's google code webpage

```/**
* Title:  Infer privacy in advanced electronic services.
*/

/**
*      Vocabulary
*/

vocabulary VocPrivAndTrust {

//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//  Vocabulary : Input model - System Model
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

type AttrSrc

type Stakeholder isa AttrSrc         // Stakeholders in the organization
type User isa Stakeholder            // User in the system : set U
type Organization isa Stakeholder    // Organizations in the system : set O

type Attribute                       // Attributes in the system : set A
type Property isa Attribute          // Properties

type AuthToken isa AttrSrc           // Authentication tokens that are
// used in the modeled system

//----------------------------------------------------------------------------
// Services & Service Policies
//----------------------------------------------------------------------------
type ServiceType                          // Services in the system : set S
type ServiceIdentifier isa AttrSrc

// A service that is represented by a service instance is characterized
// by the service type and its hosting organization
Service(ServiceIdentifier, ServiceType, Organization)

// Service policies contain four sections
type AccessPolicy
type StoragePolicy
type DistributionPolicy
type OutputPolicy

// This group of predicates specifies the service policy
OwnAuthToken(AccessPolicy,AuthToken)
RevealAttr(AccessPolicy, AttrSrc, Attribute, Stakeholder)
ProveProperty(AccessPolicy, Property, AttrSrc, Attribute, Stakeholder)
GenerateAttr(AccessPolicy, Attribute)
StoreAttr(StoragePolicy, Attribute, Stakeholder)
DistrAttrTo(DistributionPolicy, ServiceIdentifier, Attribute, Stakeholder)
OutputAttr(OutputPolicy, Attribute)

// Additional Output Policy Rules that are not implemented
//OutputCred(OutputPolicy, Credential)
//sOutputProf(OutputPolicy, Profile)

// A service policy is assigned to each service instance.  Each service
// policy is composed of an access policy, storage policy, distribution
// policy, and an output policy
ServicePolicies(ServiceIdentifier, AccessPolicy, StoragePolicy, DistributionPolicy, OutputPolicy)

//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//  Vocabulary : Input model - User Model
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

//  Trust perception of the user = two trust relations
StorageTrust(Organization)              // Set R_S
DistributionTrust(Organization)         // Set R_D

// User's initial state

// ** 1) Claim-based authentication technologies
type ClaimBasedTech
X509Tech : ClaimBasedTech
IdemixTech : ClaimBasedTech

type Credential isa AuthToken           // Credential references

CredAttr(Credential, Attribute)         // Credential's attributes
CredTech(Credential, ClaimBasedTech)    // Credential technology
CredIssuer(Credential, Organization)    // Organization that issues credential

// ** 2) Network-based technologies
//type NetworkBasedTech
//Public : NetworkBasedTech
//RestrictedAccess : NetworkBasedTech
//Private : NetworkBasedTech

//type Profile isa AuthToken                   // Profile references

//ProfAttr(Profile, Attribute, Stakeholder)  // (attr,stake) in profile
//ProfTech(Profile, NetworkBasedTech)        // Profile technology
//ProfHost(Profile, Organization)            // Profile host
//ProfAccess(Profile, Organization)          // Access Profile
//----------------------------------------------------------------------------

//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//  Vocabulary : Input model - Identifiabiltiy Model
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
type Identifier                         // Identifier set
type Identity isa Identifier            // Identity set : set I
type Pseudonym isa Identifier           // Pseudonymity set : set N

IdentifierSetAttr(Identifier, Attribute)  // Attr member of the Identity set

//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//  Vocabulary : Internal symbols
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

// Storage trust in service instance that is deduced from the
StorageTrustServInstance(ServiceIdentifier)
DistributionTrustServInstance(ServiceIdentifier)

// Service instance invocations by users
ServiceInvokedByUser(ServiceIdentifier)

// Service instance (arg 1) directly invoked by service instance (arg 2)
Successor(ServiceIdentifier, ServiceIdentifier)

// Service instance (arg1) invoked by service instance (arg2)
ServiceInvokedBy(ServiceIdentifier, ServiceIdentifier)

// Attributes that are generated by a service instance are revealed to it.
GeneratedByService(ServiceIdentifier, Attribute, Stakeholder)

// Attributes that are directly revealed when invoking a service instance
RevealedToService(ServiceIdentifier, Attribute, Stakeholder)

// Attributes that are forwarded by a service instance (arg1) to a service
// instance (arg 2) that it directly invokes
ForwardedByServiceToSucc(ServiceIdentifier, ServiceIdentifier, Attribute, Stakeholder)

// Attributes that are specified in the storage policy
ServiceStoredPolicyAttr(ServiceIdentifier, Attribute, Stakeholder)

// Attributes that are stored when revealed when invoking a service instance
ServiceStoredRevealAttr(ServiceIdentifier, Attribute, Stakeholder)

// A path between two services that contains no services that are
// distribution trusted.
UntrustedPath(ServiceIdentifier, ServiceIdentifier)

// Attributes that are distributes by preceding service instances
ServiceStoredForwardAttr(ServiceIdentifier, ServiceIdentifier, Attribute, Stakeholder)

// The sub-profiles that are built for a service instance (arg 1) invoked
// by a user invokable service (arg 2).
SubProfile(ServiceIdentifier, ServiceIdentifier, Attribute, Stakeholder)

//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
// Vocabulary : Output symbols
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

// The user profiles to construct for a user invokable service instance
UserProfile(Organization, Identifier, ServiceIdentifier, Attribute, Stakeholder)
}

/**
*      Theory
*/

theory TheoryBasicInference : VocPrivAndTrust {

//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
// Theory : behavior
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

// Storage trust of a user for a service instance is derived from the storage
// trust in the organization that hosts the service instance.
{
! si : StorageTrustServInstance(si) <- ? o st : StorageTrust(o) & Service(si,st,o).
}

// Distribution trust of a user for a service instance is derived from the
// distribution trust in the organization that hosts the service instance.
{
! si : DistributionTrustServInstance(si) <- ? o st : DistributionTrust(o) &
Service(si,st,o).
}

// Attributes that are generated by a service instance are revealed to it.
{
! si a e : GeneratedByService(si,a,e) <- ? ap sp dp op s :
ServicePolicies(si,ap,sp,dp,op) &
GenerateAttr(ap,a) &
Service(si,s,e).
}

// The attributes that are revealed to the service instance.
{
// Service policy dependent part
//  (1)   : Reveal the attributes that are specified in the access control
//          policy
//  (2)   : When proving a property, the property itself is revealed
//  (3)   : Attributes that are generated by the service instance are
//          revealed
! si a e : RevealedToService(si,a,e) <- ? ap sp dp op as :
ServicePolicies(si,ap,sp,dp,op) &
RevealAttr(ap,as,a,e).

! si prop e : RevealedToService(si,prop,e) <- ? ap sp dp op as a :
ServicePolicies(si,ap,sp,dp,op) &
ProveProperty(ap,prop,as,a,e).

! si a e : RevealedToService(si,a,e) <- GeneratedByService(si,a,e).

// Technology dependent part
//  (1)   : X509 - when proving a property, the required attributes are also
//                 revealed
//  (2)   : X509 - all attributes are revealed when using a X509
//                 certificate
//  (3)   : X509 - when proving a property, all attributes of the
//                 certificate are revealed
//  (4)   : X509 - all attributes are revealed when proving ownership
//                 of a X509 certificate
! si a e : RevealedToService(si,a,e) <- ? ap sp dp op as prop :
Credential(as) & CredTech(as,X509Tech) &
ServicePolicies(si,ap,sp,dp,op) &
ProveProperty(ap,prop,as,a,e).

! si a e : RevealedToService(si,a,e) <- ? ap sp dp op as a_0 e_0 :
Credential(as) & CredTech(as,X509Tech) &
ServicePolicies(si,ap,sp,dp,op) &
RevealAttr(ap,as,a_0,e_0) &
CredAttr(as,a) & CredIssuer(as,e).

! si a e : RevealedToService(si,a,e) <- ? ap sp dp op as prop
a_0 e_0 :
Credential(as) & CredTech(as,X509Tech) &
ServicePolicies(si,ap,sp,dp,op) &
ProveProperty(ap,prop,as,a_0,e_0) &
CredAttr(as,a) & CredIssuer(as,e).

! si a e : RevealedToService(si,a,e) <- ? ap sp dp op at :
ServicePolicies(si,ap,sp,dp,op) &
OwnAuthToken(ap,at) &
CredAttr(at,a) & CredIssuer(at,e).
}

//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
// Theory : inference
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

// A service instance (arg 2) is a successor of another service
// instance (arg 1) when the latter directly invokes the former.  This is
// derived from the distribution policy that is assigned to the latter.
// Possibly, multiple successors exist (i.e. all successors are concurrent).
{
! si succ : Successor(si,succ) <- ? ap sp dp op a e :
ServicePolicies(si,ap,sp,dp,op) &
DistrAttrTo(dp,succ,a,e).
}

// A user invokable service is no successor of any other service instance.
{
! si : ServiceInvokedByUser(si) <- ~(? pred : Successor(pred,si)).
}

// Service instance invocations propagate from one to another.
//  (1)   : A service instance (arg 2) invokes its successors (arg 1).
//  (2)   : A service instance (arg 2) invokes indirectly other
//          service instances (arg 1) = transitivity
{
! succ si : ServiceInvokedBy(succ,si) <- Successor(si,succ).
! si_2 si_0 : ServiceInvokedBy(si_2,si_0) <- ? si_1 :
ServiceInvokedBy(si_1,si_0) &
ServiceInvokedBy(si_2,si_1).
}

// Attributes that must be stored by a service instance as specified in the
// assigned storage policy.
{
! si a e : ServiceStoredPolicyAttr(si,a,e) <- ? ap sp dp op :
ServicePolicies(si,ap,sp,dp,op) &
StoreAttr(sp,a,e).
}

// All attributes that are revealed by the user to the service instance are
// stored under the assumption that there is no storage trust in the
// organization that hosts this service instance.
{
! si a e : ServiceStoredRevealAttr(si,a,e) <- RevealedToService(si,a,e).
}

// Attributes that are forwarded by a service instance (arg1) to a service
// instance (arg 2) that is directly invoked by it.
//    (1)   : Forward attributes that are specified in the distribution
//            policy
//    (2)   : Forward all revealed attributes When there is no distribution
//            trust in the organization that hosts the service instance
{
! si succ a e : ForwardedByServiceToSucc(si,succ,a,e) <- ? ap sp dp op :
DistributionTrustServInstance(si) &
ServicePolicies(si,ap,sp,dp,op) &
DistrAttrTo(dp,succ,a,e).

! si succ a e : ForwardedByServiceToSucc(si,succ,a,e) <- ? ap sp dp op ax ex :
~DistributionTrustServInstance(si) &
ServicePolicies(si,ap,sp,dp,op) &
DistrAttrTo(dp,succ,ax,ex) &
RevealedToService(si,a,e).
}

// Path where services between (start) and (end) have no distribution trust
{
! start end : UntrustedPath(start,end) <- ServiceInvokedBy(end,start) &
~(? si_x : ServiceInvokedBy(si_x,start) &
ServiceInvokedBy(end,si_x) &
DistributionTrustServInstance(si_x)).
}

// All attributes that are forwarded to a service instance (arg 1) by other
// preceding service instance caused by a user invoked service (arg 2) are
// stored under the assumption that there is no storage trust in the
// organization that hosts this service instance (arg 1)
//  (1)   : when service instance (arg 1) is successor of a user invoked
//          service
//  (2)   : when service instance (arg 1) is successor of source
//  (3)   : in case of the user invoked service is the source of attributes
//  (4)   : in case other services in the path are the source of attributes
{
! si su a e : ServiceStoredForwardAttr(si,su,a,e) <-
ServiceInvokedByUser(su) &
ForwardedByServiceToSucc(su,si,a,e).

! si su a e : ServiceStoredForwardAttr(si,su,a,e) <- ? src :
ServiceInvokedByUser(su) &
ServiceInvokedBy(src,su) &
ForwardedByServiceToSucc(src,si,a,e).

! si su a e : ServiceStoredForwardAttr(si,su,a,e) <- ? succ :
ServiceInvokedByUser(su) &
UntrustedPath(su,si) &
ServiceInvokedBy(si,succ) &
ForwardedByServiceToSucc(su,succ,a,e).

! si su a e : ServiceStoredForwardAttr(si,su,a,e) <- ? src succ :
ServiceInvokedByUser(su) &
UntrustedPath(src,si) &
ServiceInvokedBy(src,su) &
ServiceInvokedBy(si,succ) &
ForwardedByServiceToSucc(src,succ,a,e).
}

// Store all attributes in the sub profile that are the causation of the
// service instance (arg 1) invoked (directly or indirectly) by a user
// invoked service (arg 2).  Three attributes sources exist, namely
//  (1)   : attributes specified in the storage policy of a
//          user invoked service
//  (2)   : attributes revealed by the user (if no storage trust) of a user
//          invoked service
//  (3)   : attributes specified in the storage policy
//  (4)   : attributes revealed by the user (if no storage trust)
//  (5)   : attributes forwarded by preceding service instance (if no storage
//          trust).
{
! su a e :    SubProfile(su,su,a,e) <- ServiceInvokedByUser(su) &
ServiceStoredPolicyAttr(su,a,e).
! su a e :    SubProfile(su,su,a,e) <- ~StorageTrustServInstance(su) &
ServiceInvokedByUser(su) &
ServiceStoredRevealAttr(su,a,e).
! si su a e : SubProfile(si,su,a,e) <- ServiceInvokedByUser(su) &
ServiceInvokedBy(si,su) &
ServiceStoredPolicyAttr(si,a,e).
! si su a e : SubProfile(si,su,a,e) <- ~StorageTrustServInstance(si) &
ServiceInvokedByUser(su) &
ServiceInvokedBy(si,su) &
ServiceStoredRevealAttr(si,a,e).
! si su a e : SubProfile(si,su,a,e) <- ServiceInvokedByUser(su) &
ServiceInvokedByUser(su) &
ServiceInvokedBy(si,su) &
ServiceStoredForwardAttr(si,su,a,e).
}

// Merging sub profiles to user profiles kept by organization (arg 1) linked
// to an identifier (arg 2) that are the causation of a user invoked service
// (arg 3).
//  (1)   : User profiles are constructed by sub profiles
//  (2)   : Merged user profiles can be linked to newly formed identifiers
//          that were partially present in different sub profiles.
{
! o id su a e  : UserProfile(o,id,su,a,e) <- ? si s :
SubProfile(si,su,a,e) &
Service(si,s,o) &
~(? a_x : IdentifierSetAttr(id,a_x) &
~(? e_x : SubProfile(si,su,a_x,e_x))).
! o id su a e : UserProfile(o,id,su,a,e) <-  ? id_x :
UserProfile(o,id_x,su,a,e) &
~(? a_x : IdentifierSetAttr(id,a_x) &
~(? e_x : UserProfile(o,id_x,su,a_x,e_x))).
}
}

/**
*      Input model of the web shop
*/

structure StructInputPrivAndTrust : VocPrivAndTrust {

//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
// System model
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
AttrSrc = {
User;
Government; University; WS; PS;
BasicIDCard; PrivIDCard; StudentCard;
BasicPurchaseServ; PrivPurchaseServ;
BasicReductionPurchaseServ; PrivReductionPurchaseServ;
DeliveredServ;
DeliveryRequestServ; DeliveryServ;
}

Stakeholder = {
User;
Government; University; WS; PS;
}

User = {
User;
}

Organization = {
Government; University; WS; PS;
}

Attribute = {
Name; Address; DoB; SSN; Institute; OrderNr; URL; EMail;
AgeLimit;
}

Property = {
AgeLimit;
}

// Services & Service Policies
ServiceType = { Purchase; Delivered; DeliveryRequest; Delivery; }

ServiceIdentifier = {
BasicPurchaseServ; PrivPurchaseServ;
BasicReductionPurchaseServ; PrivReductionPurchaseServ;
DeliveredServ;
DeliveryRequestServ; DeliveryServ;
}

Service = {
BasicPurchaseServ,Purchase,WS;
PrivPurchaseServ,Purchase,WS;
BasicReductionPurchaseServ,Purchase,WS;
PrivReductionPurchaseServ,Purchase,WS;
DeliveredServ,Delivered,WS;
DeliveryRequestServ,DeliveryRequest,PS;
DeliveryServ,Delivery,PS;
}

AccessPolicy = {
BasicPurchaseServAP; PrivPurchaseServAP;
BasicReductionPurchaseServAP; PrivReductionPurchaseServAP;
DeliveredServAP; DeliveryRequestServAP; DeliveryServAP;
}

StoragePolicy = {
PurchaseServSP; DeliveredServSP;
DeliveryRequestServSP; DeliveryServSP;
}

DistributionPolicy = {
PurchaseServDP; DeliveredServDP;
DeliveryRequestServDP; DeliveryServDP;
}

OutputPolicy = {
PurchaseServOP; DeliveredServOP;
DeliveryRequestServOP; DeliveryServOP;
}

OwnAuthToken = {
BasicReductionPurchaseServAP,StudentCard;
PrivReductionPurchaseServAP,StudentCard;
}

RevealAttr = {
BasicPurchaseServAP,User,EMail,User;
//BasicPurchaseServAP,BasicIDCard,DoB,Government;

PrivPurchaseServAP,User,EMail,User;
//PrivPurchaseServAP,PrivIDCard,DoB,Government;

BasicReductionPurchaseServAP,User,EMail,User;
//BasicReductionPurchaseServAP,BasicIDCard,DoB,Government;

PrivReductionPurchaseServAP,User,EMail,User;
//PrivReductionPurchaseServAP,PrivIDCard,DoB,Government;

DeliveredServAP,PS,OrderNr,WS;

DeliveryRequestServAP,WS,OrderNr,WS;
DeliveryRequestServAP,WS,EMail,User;
DeliveryRequestServAP,User,Name,User;

DeliveryServAP,PS,OrderNr,WS;
DeliveryServAP,PS,Name,User;
}

ProveProperty = {
BasicPurchaseServAP,AgeLimit,BasicIDCard,DoB,Government;
PrivPurchaseServAP,AgeLimit,PrivIDCard,DoB,Government;
BasicReductionPurchaseServAP,AgeLimit,BasicIDCard,DoB,Government;
PrivReductionPurchaseServAP,AgeLimit,PrivIDCard,DoB,Government;
}

GenerateAttr = {
BasicPurchaseServAP,OrderNr;
PrivPurchaseServAP,OrderNr;
BasicReductionPurchaseServAP,OrderNr;
PrivReductionPurchaseServAP,OrderNr;
DeliveryRequestServAP,URL;
}

StoreAttr = {
PurchaseServSP,EMail,User;
PurchaseServSP,OrderNr,WS;

DeliveredServSP,OrderNr,WS;

DeliveryRequestServSP,OrderNr,WS;
DeliveryRequestServSP,EMail,User;
DeliveryRequestServSP,Name,User;
DeliveryRequestServSP,URL,PS;

// DeliveryId - no attributes are stored
}

DistrAttrTo = {
PurchaseServDP,DeliveryRequestServ,OrderNr,WS;
PurchaseServDP,DeliveryRequestServ,EMail,User;

// DeliveredIdDP - no attributes are forwarded

DeliveryRequestServDP,DeliveryServ,OrderNr,WS;
DeliveryRequestServDP,DeliveryServ,Name,User;

DeliveryServDP,DeliveredServ,OrderNr,WS;
}

OutputAttr = {
// ServPurchaseOP - no attributes output

// DeliveredIdOP - no attributes output

DeliveryRequestServOP,URL;

// DeliveryIdOP - no attributes output
}

ServicePolicies = {
BasicPurchaseServ,BasicPurchaseServAP,PurchaseServSP,
PurchaseServDP,PurchaseServOP;

PrivPurchaseServ,PrivPurchaseServAP,PurchaseServSP,
PurchaseServDP,PurchaseServOP;

BasicReductionPurchaseServ,BasicReductionPurchaseServAP,PurchaseServSP,
PurchaseServDP,PurchaseServOP;

PrivReductionPurchaseServ,PrivReductionPurchaseServAP,
PurchaseServSP,PurchaseServDP,PurchaseServOP;

DeliveredServ,DeliveredServAP,DeliveredServSP,DeliveredServDP,
DeliveredServOP;

DeliveryRequestServ,DeliveryRequestServAP,DeliveryRequestServSP,
DeliveryRequestServDP,DeliveryRequestServOP;

DeliveryServ,DeliveryServAP,DeliveryServSP,DeliveryServDP,
DeliveryRequestServOP;
}

//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
// User model
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

// Trust perception by the user
StorageTrust = { PS; }

DistributionTrust = { WS; }

// Initial state of the user
ClaimBasedTech = { X509; Idemix; }
X509Tech = X509
IdemixTech = Idemix
Credential = { BasicIDCard; PrivIDCard; StudentCard; }

CredAttr = {
PrivIDCard,SSN;
}

CredTech = {
BasicIDCard,X509; PrivIDCard,Idemix; StudentCard,X509;
}

CredIssuer = {
BasicIDCard,Government; PrivIDCard,Government; StudentCard,University;
}

//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
// Identifiability model
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
//++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Identifier = { Identity1; Nym1; Nym2; Nym3; Nym4;}

Identity = { Identity1; }

Pseudonym = { Nym1; Nym2; Nym3; Nym4; }

IdentifierSetAttr = {
Nym1,SSN; Nym2,OrderNr; Nym3,URL; Nym4,EMail;
}
}

//query Query1 : VocPrivAndTrust {
//    { o id si a e : UserProfile(o,id,si,a,e) }
//}

procedure main() {
stdoptions.nbmodels = 1
models = modelexpand(TheoryBasicInference,StructInputPrivAndTrust)
//models = query(Query1,StructInputPrivAndTrust)
printmodels(models)
}```
Last Updated on Thursday, 25 September 2014 08:39