>
> How to convert pred arrives to a function that returns Harbor?  When I convert it into the following fcn I get a type error?
>
> fun arrives (h,h': Harbor, s: Ship) :Harbor  {
>   (can_arrive[s,h]  and consistent[h] and consistent[h']  and s in h'.ship) => h'
> }

When that condition is true, you want to return h'
When that condition is false, what do you want it to return?

I'm guessing you want it to return h
If so, you need to supply the ELSE part:

fun arrives (h,h': Harbor, s: Ship) :Harbor  {
  (can_arrive[s,h]  and consistent[h] and consistent[h']  and s in h'.ship) => h' else h
}

Thanks!

How to write this rsl line in alloy:

occupancy(b2, leaves(s,b1,h)) ≡  if b1 = b2 then vacant else occupancy(b2,h) end

I was getting a type error:

fact {
   all h:Harbor, s:Ship, b1,b2:Berth | occupied[b2,docks[h,s,b1]] => b1=b2 => s else occupied[b2,h]
}

You'll have to clarify what you mean to write. In particular, you have to be careful
when you want a formula (which has a true and false value) and when you want an expression (which is a set of zero or more tuples)

The main formula you wrote is
   occupied[..] => b1=b2 => s else occupied[b2,h],
which is parsed as
   occupied[..] => (b1=b2 => s else occupied[b2,h])
following the standard C/C++/Java/C# convention of attaching the ELSE clause
to the nearest preceding conditional that doesn't have an ELSE clause.

occupied[...] is a function. But you're saying "if occupied[...] is true, then something something something".
Well, occupied[...] is a function and can never be true.

Yes you are correct.  Occupied is a fcn that returns Ship or Vacant.  So, in RSL, it says:

occupancy(b2, leaves(s,b1,h)) ≡ if b1 = b2 then s else occupancy(b2,h) end

and leaves is a fcn that returns type Harbor like arrives fcn

It sounds like what you mean is, the value returned by occupancy[...]
is the same as the value returned by "if b1=b2 then return s else return occupancy(b2,h)".

If that's the case, the Alloy syntax for that is:
all h:Harbor, s:Ship, b1,b2:Berth | occupied[b2, leaves[s,b1,h]] = (b1=b2 => s else occupied[b2,h])

Sincerely,
Felix Chang
Alloy4 Lead Developer

I've modified the same program as follows.  I am thinking of two different states of Harbor.  One is can_arrive where the ship is not in the pool and berth but is only in the harbor. Hence, the ship can_arrive.  Second state is it has indeed arrived which means the ship is on waiting in the pool.  The two different distinctions have been given in the pred arrives (h, h').  But there is no instance found.  Which probably means the system is not able to differentiate between the two harbors.  How can I accomplis this?

sig Harbor{
    ship: set Ship,
   pool: one Pool,
   berth: some Berth
}
{
   ( all s1,s2:Ship | ( s1 in pool.waiting and s2  in berth.docked => s1 != s2 )  and ( s1 in berth.docked and s2 in berth.docked => s1 != s2 )  )
}

sig Ship{
   sizeship: Int
}
{sizeship > 0}

one sig Pool  {
   waiting: set Ship,
   ship: some Ship
}

sig Berth {
   fits: set Ship,
   ship: some Ship,
   sizeberth: Int,
   docked: one Ship + Vacant
}
{(all s:Ship | s in fits) and (sizeberth > 0) }

one sig Vacant {}

pred fits(s: Ship, b: Berth) {
   b.sizeberth >= s.sizeship
}

pred waiting(s: Ship, h: Harbor) {
   s in h.pool.ship and s ! in h.ship and s ! in h.berth.ship
}

fun occupied [b: Berth, h: Harbor] : Ship + Vacant {
   b.docked
}

pred can_arrive (s: Ship, h: Harbor) {
   s ! in h.pool.waiting and s ! in h.berth.docked
}

pred is_docked(s: Ship, h: Harbor)  {
   some b:Berth | occupied[b,h] = s
}

pred consistent(h: Harbor) {
   all s:Ship | not (waiting[s, h] and is_docked[s, h] ) and
   ( all b1,b2: Berth | occupied[b1,h] = s and occupied[b2,h] = s => b1=b2 ) and
   ( all b: Berth | occupied[b,h] = s => fits[s,b] )
}

pred arrives (h,h': Harbor, s: Ship) {
  (can_arrive[s,h]  and consistent[h] and consistent[h'] and h'.pool.waiting)
}

// facts

fact N1 {
   all h,h':Harbor, s1, s2:Ship | arrives[h,h',s1] => waiting[s2, h'] => ( s1=s2 or waiting[s2,h] )
}

fact N3 {
   all h,h':Harbor, s:Ship, b:Berth | arrives[h,h',s] => occupied[b,h'] = occupied[b,h]
}

fact {
   all h,h':Harbor, s:Ship | arrives[h,h',s] => consistent[h']
}

run arrives for 3 but 2 Harbor