I’m trying to model a presentation with ordered slides, with no slide appearing in two presentations, and every slide appearing in a presentation.

sig Presentation {
// At most #Int arrows, exactly #Slide arrows, each Int used at most once
slides: Int one -> lone Slide
} {
#slides > 1
}
sig Slide {} {Slide = Presentation.slides[Int]}
run {} for 5 but exactly 2 Presentation

I’m having trouble expressing the part about no slide being in two presentations. I’ve tried things like:

fact { all p1, p2: Presentation | no p1.slides[Int] & p2.slides[Int] }
fact { all slide: Slide, p1, p2: Presentation | p1 in slides.slide.Int and p2 in slides.slide.Int implies p1=p2 }

But adding those facts just causes the run command to find no instances.

What am I doing wrong? Should I move to another way of describing the ordering of slides? I’m using this way (slides: Int-> Slide) because I’m hoping to later implement reordering with limitations (a slide may refer to an earlier slide, and may not be moved ahead of it).

Hi,
technically, what you did with slides is encode a list of slides. I would first suggest to separate the notion of list (which could be modelled using a generic module) from that of presentation.
Now, as a matter of fact, lists already exist in the Alloy library in 3 forms, you may look at them to get inspiration or just reuse one of them. Essentially:

seqrel represents a list as a relation from a set of indices to a set of elements

sequence represents a list as a signature containing such a relation (thus you may manipulate lists more easily if needed)

sequniv is rougly like seqrel except that you never open it explicitly, instead you use the keyword seq to declare a list and then can use functions and predicates from sequniv as needed.

All these modules implement a function elems that will allow to retrieve the set of elements. You may use it to specify fact that bothers you.

Hope this helps; otherwise please do not hesitate to touch base.

open util/sequence[Slide]
sig Presentation {
slides: Seq
}
sig Slide {}

fails with

Starting the solver...
.
Name cannot be resolved; possible incorrect
function/predicate call; perhaps you used ( ) when you
should have used [ ]
This cannot be a correct call to pred sequence/add.
The parameters are
s: {sequence/Seq}
e: {this/Slide}
added: {sequence/Seq}
so the arguments cannot be
sequence/inds[s] (type = {sequence/SeqIdx})
Int[1] (type = {Int})
This cannot be a correct call to fun integer/add.
The parameters are
n1: {Int}
n2: {Int}
so the arguments cannot be
sequence/inds[s] (type = {sequence/SeqIdx})
Int[1] (type = {Int})

and the highlighted line is part of

/** added is the result of appending e to the end of s */
pred add [s: Seq, e: elem, added: Seq] {
added.startsWith[s]
added.seqElems[s.afterLastIdx] = e
#added.inds = #s.inds.add[1]
}

Oops, right, there’s a bug in the last version(s) of alloy regarding the typing of sequence. Please either use seqrel or the keyword seq, as in the examples below:

open util/seqrel[Slide]
sig Presentation {
slides: SeqIdx -> Slide
} { isSeq[slides] }
sig Slide {}

and

sig Presentation {
slides: seq Slide
}
sig Slide {}

Unfortunately, I’m still stuck when trying to define that a slide only belongs to one Presentation.
I’m mostly trying variants of fact { all disj p1, p2: Presentation | no p1.slides[SeqIdx] & p2.slides[SeqIdx] } but adding this prevents the solver from generating any instances.

I do have instances so perhaps you forgot to tell us about an additional constraint that you inadvertently left in your model? Here is mine:

open util/seqrel[Slide]
sig Presentation {
slides: SeqIdx -> Slide
} { isSeq[slides] }
sig Slide {}
fact { all disj p1, p2: Presentation | no p1.slides[SeqIdx] & p2.slides[SeqIdx] }
// or:
// fact { all disj p1, p2: Presentation | no p1.slides.elems & p2.slides.elems}
run { some slides } for 3 but exactly 2 Presentation

I managed to get instances, after some cleanups, and ended up with what you’ve posted. Now is it possible to remove multiple links between a presentation and a slide?
I’m seeing something similar to

Sure you can, it’s very easy with one of the functions of util/seqrel (there’s an hint in the next sentence). Now the question, which is a domain-related question rather than a formal one, is why would it be forbidden to have duplicate slides in a presentation? It’s actually perfectly feasible in any presentation tool. The more you allow strange but possible instances, the stronger your checks will be.

open util/seqrel[Slide]
sig Presentation {
slides: SeqIdx -> Slide
} {
isSeq[slides]
!hasDups[slides]
}
sig Slide {}
fact { all disj p1, p2: Presentation | no p1.slides.elems & p2.slides.elems}
run { some slides } for 5 but exactly 2 Presentation

As for duplicates, it was more me trying to push my ideas to the end
The duplication is possible in our case (and powerpoint/google slides work similarly) but it’s a copy by value, not copy by reference, so you end up with a whole new slide that continues to exist independently of the original.