# How to check to see if a file has gone through same state

**URL:** <https://alloytools.discourse.group/t/how-to-check-to-see-if-a-file-has-gone-through-same-state/361>\
**Category:** Questions\
**Created:** [June 14, 2023, 8:26pm UTC](https://alloytools.discourse.group/t/how-to-check-to-see-if-a-file-has-gone-through-same-state/361 "2023-06-14T20:26:21Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![Adam](https://avatars.discourse-cdn.com/v4/letter/a/4af34b/32.png) [@Adam](https://alloytools.discourse.group/u/Adam)\
**Post date:** [June 14, 2023, 8:26pm UTC](https://alloytools.discourse.group/t/how-to-check-to-see-if-a-file-has-gone-through-same-state/361/1 "2023-06-14T20:26:21Z")

</div>

Hi,

I am new to using Alloy 6 and just was following along with some simple Recycling bin examples on this website I found. Everything in the model is fine I just was wondering how to assert a case I thought of which is how would I check if its possible that a specific file that was already deleted was attempted to be deleted again. Thanks for any help.

var sig File{}  
var sig Trash in File{}

fact init {  
no Trash  
}  
pred empty{  
some Trash and  
after no Trash and // why ands are used here but not in delete?  
File’ = File - Trash  
}  
pred delete [f: File]{  
not f in Trash //can this be no f in Trash?  
Trash ’ = Trash + f  
File’ = File  
}  
pred restore [f: File] {  
f in Trash  
Trash’ = Trash - f  
File’ = File  
}

pred idle {  
File’ = File  
Trash’ = Trash  
}

fact transition {  
always (empty or (some f: File | delete[f] or restore[f]) or idle) //you are always going to be in empty or deleting or restoring  
}

//I want to check if there is a case in which you delete the same file twice or can this be done rather?  
assert delete\_same\_file {   
}

---

<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:** [June 15, 2023, 7:10am UTC](https://alloytools.discourse.group/t/how-to-check-to-see-if-a-file-has-gone-through-same-state/361/2 "2023-06-15T07:10:20Z")

</div>

You want to see such a scenario, so it’s easier to think in terms of `run`. Here’s a hint: you’re asking whether, at some point in the future, there’s a file that’s deleted and then, strictly later, it’s deleted again.

---

<div class="post-metadata">

**Author:** ![Adam](https://avatars.discourse-cdn.com/v4/letter/a/4af34b/32.png) [@Adam](https://alloytools.discourse.group/u/Adam)\
**Post date:** [June 15, 2023, 5:28pm UTC](https://alloytools.discourse.group/t/how-to-check-to-see-if-a-file-has-gone-through-same-state/361/3 "2023-06-15T17:28:22Z")

</div>

Thanks I will try and do that. Why run though run to me I have thought of as I want to visualize a scenario and asserts are more useful for checking something if its ever possible right? Just trying to learn Alloy and this way of thinking so if you have any insight to how you came to Run as the better use vs Assert and check I would value 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:** [June 16, 2023, 2:53pm UTC](https://alloytools.discourse.group/t/how-to-check-to-see-if-a-file-has-gone-through-same-state/361/4 "2023-06-16T14:53:40Z")

</div>

Let us write `S` for our spec and `P` for the property analyzed by a command, _in scope_ `k`.

Then `run P` asks whether _there is_ an instance in scope `k` that satisfies `S && P`. This can be written summarily as the problem called `SAT_k(S && P)`

While `check P` asks whether _all_ instances in scope `k` satisfy `S => P`. Logically, this the same as asking whether _there is **no** _ instance in scope `k` that satisfies `S && not P`, _i.e._ `not SAT_k(S && not P)`, or `UNSAT_k(S && not P)`.

So, if you have a solver that knows how to solve `SAT_k` problems, you can solve both `run` and `check` commands the same way.

Notice finally that if you get an instance from a `check`, this is in practice a counter-example (as you asked for **no** instance and you still got one), while if you get an instance from a `run`, what you get is what we would colloquially call a scenario.

Here, you want to see _“if there is a case …”_, that if there is an instance such that… So `run` applies straightforwardly. Due to the duality shown above, you could use a `check` command, but you would then have to add a negation, saying what you _don’t_ want to observe, that is two deletes on the same file, and expect to get a counter-example.

EDIT: fixed typo with UNSAT.