You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The scenario that is described by the second run in the model below ("delete 1 file among 2 files and then empty the trash") cannot be found using fork from an empty run (or from the first run in the model).
The bug is in Electrum 2.1 rc2 and Electrum 2.1 rc1 but not in Electrum 2.0.
//***************************
// Electrum model of a simple file system
var sig File {}
var sig Trash in File {}
pred delete [f: File] {
f not in Trash
Trash' = Trash + f
File' = File
}
pred restore [f: File] {
f in Trash
Trash' = Trash - f
File' = File
}
pred empty {
some Trash
no Trash'
File' = File - Trash
}
pred do_nothing {
File' = File
Trash' = Trash
}
pred restoreEnabled [f:File] {
f in Trash
}
fact Behaviour {
no Trash
always {
(some f: File | delete[f] or restore[f]) or empty or do_nothing
}
}
simplerun: run {some disj f1,f2:File | delete[f1]}
scenario: run {some disj f1,f2:File | delete[f1] and after empty}
//***************************
The text was updated successfully, but these errors were encountered:
The scenario that is described by the second run in the model below ("delete 1 file among 2 files and then empty the trash") cannot be found using fork from an empty run (or from the first run in the model).
The bug is in Electrum 2.1 rc2 and Electrum 2.1 rc1 but not in Electrum 2.0.
//***************************
// Electrum model of a simple file system
var sig File {}
var sig Trash in File {}
pred delete [f: File] {
f not in Trash
Trash' = Trash + f
File' = File
}
pred restore [f: File] {
f in Trash
Trash' = Trash - f
File' = File
}
pred empty {
some Trash
no Trash'
File' = File - Trash
}
pred do_nothing {
File' = File
Trash' = Trash
}
pred restoreEnabled [f:File] {
f in Trash
}
fact Behaviour {
no Trash
always {
(some f: File | delete[f] or restore[f]) or empty or do_nothing
}
}
simplerun: run {some disj f1,f2:File | delete[f1]}
scenario: run {some disj f1,f2:File | delete[f1] and after empty}
//***************************
The text was updated successfully, but these errors were encountered: