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

Questions
1

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

2

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.

3

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!

4

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.