# Modeling a presentation with ordered slides

**URL:** <https://alloytools.discourse.group/t/modeling-a-presentation-with-ordered-slides/326>\
**Category:** Uncategorized\
**Created:** [March 21, 2023, 9:20am UTC](https://alloytools.discourse.group/t/modeling-a-presentation-with-ordered-slides/326 "2023-03-21T09:20:02Z")\
**Posts on this page:** 9\
**Page:** 1

<div class="post-metadata">

**Author:** ![marko](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/marko/32/58_2.png) [@marko](https://alloytools.discourse.group/u/marko)\
**Post date:** [March 21, 2023, 9:20am UTC](https://alloytools.discourse.group/t/modeling-a-presentation-with-ordered-slides/326/1 "2023-03-21T09:20:02Z")

</div>

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.

```auto
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:

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

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [March 21, 2023, 1:27pm UTC](https://alloytools.discourse.group/t/modeling-a-presentation-with-ordered-slides/326/2 "2023-03-21T13:27:23Z")

</div>

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](https://alloytools.org/quickguide/seq.html) 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.

---

<div class="post-metadata">

**Author:** ![marko](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/marko/32/58_2.png) [@marko](https://alloytools.discourse.group/u/marko)\
**Post date:** [March 21, 2023, 9:36pm UTC](https://alloytools.discourse.group/t/modeling-a-presentation-with-ordered-slides/326/3 "2023-03-21T21:36:35Z")

</div>

Thanks!  
How would I use `sequence` ?

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

```

fails with

```auto
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

```auto
/** 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]
}

```

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [March 22, 2023, 8:42am UTC](https://alloytools.discourse.group/t/modeling-a-presentation-with-ordered-slides/326/4 "2023-03-22T08:42:41Z")

</div>

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:

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

```

and

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

```

---

<div class="post-metadata">

**Author:** ![marko](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/marko/32/58_2.png) [@marko](https://alloytools.discourse.group/u/marko)\
**Post date:** [March 22, 2023, 10:02am UTC](https://alloytools.discourse.group/t/modeling-a-presentation-with-ordered-slides/326/5 "2023-03-22T10:02:43Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [March 22, 2023, 10:29am UTC](https://alloytools.discourse.group/t/modeling-a-presentation-with-ordered-slides/326/6 "2023-03-22T10:29:15Z")

</div>

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:

```auto
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

```

---

<div class="post-metadata">

**Author:** ![marko](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/marko/32/58_2.png) [@marko](https://alloytools.discourse.group/u/marko)\
**Post date:** [March 22, 2023, 10:36am UTC](https://alloytools.discourse.group/t/modeling-a-presentation-with-ordered-slides/326/7 "2023-03-22T10:36:58Z")

</div>

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

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

```

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [March 22, 2023, 10:43am UTC](https://alloytools.discourse.group/t/modeling-a-presentation-with-ordered-slides/326/8 "2023-03-22T10:43:00Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![marko](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/marko/32/58_2.png) [@marko](https://alloytools.discourse.group/u/marko)\
**Post date:** [March 22, 2023, 2:49pm UTC](https://alloytools.discourse.group/t/modeling-a-presentation-with-ordered-slides/326/9 "2023-03-22T14:49:23Z")

</div>

The hint worked, thanks!

Now the model is this:

```auto
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.

Thanks for the help!