Modeling a presentation with ordered slides

1

Hi!

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).

2

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.

1 Like
3

Thanks!
How would I use sequence ?

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]
}
4

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 {}
5

Thanks! The use of seqrel helped.

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.

Do you have any advice for that?

6

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
7

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

┌─────────────────┬─────────────────────┐
│this/Presentation│slides               │
├─────────────────┼──────────────┬──────┤
│Presentation⁰    │seqrel/SeqIdx⁰│Slide¹│
│                 ├──────────────┼──────┤
│                 │seqrel/SeqIdx¹│Slide¹│
│                 ├──────────────┼──────┤
│                 │seqrel/SeqIdx²│Slide¹│
└─────────────────┴──────────────┴──────┘
8

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.

9

The hint worked, thanks!

Now the model is this:

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 :slight_smile:
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.

Thanks for the help!

1 Like