Alloy time dependent initialisation

1

Find below a discussion topic on initialization of time dependent sets with Alloy

Different behavior during initialization when using integers:

Version 1: initialization of a State to zero component with addition of an extra component

module Test
open util/ordering[Time] as T
sig Time {}

let dynamic[x] = x one-> Time
let dynamicLess[x] = x lone-> Time
let dynamicSet[x] = x -> Time

sig Farm {}
abstract sig Items extends Farm {}

one sig Farmer extends Items {}
lone sig Chicken extends Items {}
lone sig Grain extends Items {}
lone sig Fox extends Items {}
lone sig Wolf extends Items {}

one abstract sig State {
item: dynamicSet[Items],
next: one State
}

pred InitState[c:State,t:Time] { no c.item.t }

let addItem[c,itm, t1,t2]= c.item=c.item+itm->t2-itm->t1

// set all initial state to empty
// add one element to the next to initial state
// impose that the first time is the minimum time and the second time
// is its successor
// If satisfied, add an element to the state
fact{
all c:State| InitState[c,T/first]
all c:State|all t1,t2:Time| one itm:Items|
(t1=min[t1]) and
(#c.item.t1=0) and
(t2=min[t1].next) => addItem[c,itm,t1,t2]
}

pred show {}

run show for 8 but 4 Time, 1 State

Version 2 removing the state count during initialization:

module Test
open util/ordering[Time] as T
sig Time {}

let dynamic[x] = x one-> Time
let dynamicLess[x] = x lone-> Time
let dynamicSet[x] = x -> Time

sig Farm {}
abstract sig Items extends Farm {}

one sig Farmer extends Items {}
lone sig Chicken extends Items {}
lone sig Grain extends Items {}
lone sig Fox extends Items {}
lone sig Wolf extends Items {}

one abstract sig State {
item: dynamicSet[Items],
next: one State
}

pred InitState[c:State,t:Time] { no c.item.t }

let addItem[c,itm, t1,t2]= c.item=c.item+itm->t2-itm->t1

// set all initial state to empty
// add one element to the next to initial state
// impose that the first time is the minimum time and the second time
// is its successor
// If satisfied, add an element to the state
fact{
all c:State| InitState[c,T/first]
all c:State|all t1,t2:Time| one itm:Items|
(t1=min[t1]) and
// (#c.item.t1=0) and
(t2=min[t1].next) => addItem[c,itm,t1,t2]
}

pred show {}

run show for 8 but 4 Time, 1 State

2

The correct version requires to instantiate T:

module Test
open util/ordering[Time] as T
sig Time {}

let dynamic[x] = x one-> Time
let dynamicLess[x] = x lone-> Time
let dynamicSet[x] = x -> Time

sig Farm {}
abstract sig Items extends Farm {}

one sig Farmer extends Items {}
lone sig Chicken extends Items {}
lone sig Grain extends Items {}
lone sig Fox extends Items {}
lone sig Wolf extends Items {}

one abstract sig State {
item: dynamicSet[Items],
next: one State
}

pred InitState[c:State,t:Time] { no c.item.t }

let addItem[c,itm, t1,t2]= c.item=c.item+itm->t2-itm->t1

// set all initial state to empty
// add one element to the next to initial state
// impose that the first time is the minimum time and the second time
// is its successor
// If satisfied, add an element to the state
fact{
all c:State| InitState[c,T/first]
all c:State| one itm:Items|
let t1=T/first,t2=t1.next {
(t1=min[t1]) and
(#c.item.t1=0) and
(t2=min[t1].next) => addItem[c,itm,t1,t2]
}
}

pred show {}

run show for 8 but 4 Time, 1 State

3

A time dependent river crossing model is then:
// Ref1: Daniel Jackson Software Abstractions 2012, p52-67
// Ref2: https://alloytools.org/tutorials/online/frame-RC-1.html
// Ref3: Gilles Dowek, les demonstrations et les algorithmes, Ch 8
// River Crossing Model
//https://alloytools.discourse.group/t/alloy-time-dependent-initialisation/
//
module TimeInAlloyExample
open util/ordering[Time] as T
abstract sig Time {}

let dynamic[x] = x one-> Time
let dynamicLess[x] = x lone-> Time
let dynamicSet[x] = x -> Time

abstract sig Object {}

one sig Farmer,Chicken,Grain,Fox extends Object {}{}
// Defines what eats what
sig eating {eats:Object->Object}{ eats = Fox->Chicken + Chicken->Grain }

// Store the Objects into States
abstract sig State {
item: dynamicSet[Object],
}
// Define near and far side of the river
one sig near, far extends State {}

// Define the initial state all objects are in the near side of the river
fact InitState {
near.item = near.item+Object->T/first &&
far.item=far.item-Object->T/first
}

// Define goal to have all objects in the far side of the river
pred goal {
some t:Time-T/first|
near.item = near.item-Object->t &&
far.item=far.item+Object->t
}

/* crossRiver transitions between states
at most one Object moves across the river
Ref [2]
*/
pred crossRiver[from,to: State,t:Time] {
((
(from.item=from.item+from.item.(t.prev)->t
-Farmer->t- from.item.t.(eating.eats)->t
)
) or (
one x: from.item.(t.prev)-Farmer | {
(from.item=from.item+from.item.(t.prev)->t
-x->t-Farmer->t-from.item.t.(eating.eats)->t
)}
))}

pred NoEating[t:Time] {
{
(not(Farmer in near.item.t) =>
not(Chicken in near.item.t and Fox in near.item.t) and
not(Chicken in near.item.t and Grain in near.item.t)) and
(not(Farmer in far.item.t) =>
not(Chicken in far.item.t and Fox in far.item.t) and
not(Chicken in far.item.t and Grain in far.item.t))
}
}

// define transitions between states
// Check for constructive constraints [Ref3]
// Make move
fact stateTransition {
all t:Time-T/last {
( (near.item.t+far.item.t=Object) and
(near.item.t&far.item.t=none) and
NoEating[t]) and
(( (Farmer->t in near.item) and
crossRiver [near, far,t.next]) or
( (Farmer->t in far.item) and
crossRiver [far, near,t.next]))
}
}

run goal for 8