:::warning
Announcements
- Modeling 1 back soon (now back).
- Modeling 2 due tomorrow.
- Pair form for Modeling 3: https://forms.gle/mqJRY2ggjC4QRUrp7
- (Short) press release reading for Thursday
:::

In Alloy 6, you can still use almost all of the Alloy features documented in the textbook to describe static systems or to manually specify expliti events and traces.

However, you can now *also* model systems that change over time by marking certain sigs as *variable*. Once any sig in a model is marked `var`, the instances the Analyzer finds will be *traces* that describe infinite sequences of states. Each state is like an instance in static Alloy, in that it is an assignment of specific atoms to all sigs and fields.

:::info
Note this change also applies to `univ` and `iden`: these are variable sets that change over time.
:::

Two types of properties:

- Safety properties: something bad never happens.
- Liveness properties: something good eventually happens.

Examples of safety properties?

- A call to `malloc` never returns overlapping live blocks
- A user can't read data on a filesystem unless the permissions allow it
- The self-driving car never hits a wall
- If a user deletes a file then restores it, it’s like they never did anything to the file. As we saw last class, this property involves two events, so we need 3 states to talk about it.

Examples of liveness properties?
- Every call to `malloc` eventually has a valid block returned
- Every open file is eventually closed
- When a thread attempts to aquire a lock, it eventually can enter the critical section

Safety properties have **finite** counterexamples, liveness properties do not: they require an infinite trace (often represented by a looping/lasso trace) as a counterexample.

## Alloy 6's temporal operators!

We'll start with just the basic temporal operators:

Note: current nodes are shown in green

---
`always P`: P is currently true and true in all future steps.

Example:

graph LR
1[P]-->2[P]-->3[P]-->3[P]

style 1 fill:#6fc276

---
`historically P`: P is currently true and true in all past steps

Example:

graph LR
1[P]-->2[P]-->3[P]-->3[P]

style 3 fill:#6fc276

---

`eventually P`: P is currently true or true in at least one future step.

Example:

graph LR
1[!P]-->2[!P]-->3[P]-->3[P]

style 1 fill:#6fc276

---

`once P`: P is currently true or was true in at least one past step.

Example:

graph LR
1[P]-->2[!P]-->3[!P]-->3[!P]

style 3 fill:#6fc276

---

`after P`: P is true in the next step. Conceptually, read this as: "immediately after this step, P will be true".

Example:

graph LR
1[!P]-->2[P]-->3[!P]-->3[!P]

style 1 fill:#6fc276

---

`before P`: P was true in the prir step. Conceptually, read this as: "immediately before this step, P was true".

Example:

graph LR
1[P]-->2[!P]-->3[!P]-->3[!P]

style 2 fill:#6fc276

---

`Q releases P`: P is true in all states or true in all states before a state where Q is true, then P may become false.

Examples:

graph LR
1[P !Q]-->1[P !Q]

style 1 fill:#6fc276

graph LR
1[P !Q]-->2[!P Q]-->3[!P Q]-->3[!P Q]

style 1 fill:#6fc276

---

`P until Q`: Equivalent to (Q releases P) and eventually Q.

graph LR
1[P !Q]-->2[!P Q]-->3[!P Q]-->3[!P Q]

style 1 fill:#6fc276

---

Our continued Trash model from last time:

var sig File {} // var: set changes over time

var sig Trash in File {}

pred deleteFile(f: File) {
   f not in Trash // this trash is the current moment
   Trash'  = f +Trash   // trash prime, trash tick
                                 // refers to the state immediately
                                 // after the current state
  // simplify: no new files added/perm deleted while
  // this is happening
  File' = File
  // obligated to talk about every var sig or field
}

// the prime ' syntax is used in the textbook, but 
// before it was a keyword

pred restoreFile(f: File) {
   f in Trash
   Trash' = Trash - f
   File' = File
}

pred doNothing {
  File' = File
  Trash' = Trash
}

pred emptyStartingTrash(t: Trash) {
   no t
}

fact validTraces {
    // not invoking time: this applies to the initial state
   emptyStartingTrash[Trash]
   always (doNothing or (some f: File | 
         deleteFile[f] or restoreFile[f]))

}

assert deleteThenRestore {
   always {
       all f: File | 
          // set up the condition as an implication
        (deleteFile[f] and after restoreFile[f]) =>
         // check for what we assume/want
        {
		Trash'' = Trash // this succeeds
                File'' = File
		// Trash''' = Trash // this fails, as we expect
        }
  }
}
check deleteThenRestore

// Group exercise:

// Express and then check both of these properties
// 1. "all restored file have to have been previously deleted"
// 2. "all deleted files must be restored"

// Write an assert, check it, describe counterexample if there is one 
// hint: one should have counterexample, the other should not
assert restorePreviouslyDeleted {
   always { all f: File | restoreFile[f] => once deleteFile[f] } 
}
check restorePreviouslyDeleted

assert deleteMustBeRestored {
   always { all f: File | deleteFile[f] => eventually restoreFile[f]}
}
check deleteMustBeRestored


run { eventually some f: File | restoreFile[f] }