Modeling Desktops and Software Operations
Desktop model
Roger L. Costello
March 24, 2018
icon2
Desktop0
Desktop1
cut
icon3
Desktop2
paste
icon3
icon1
icon3
It’s time to model software
•
In the previous examples there was just one or a small number of
solutions (instances) satisfying the constraints.
•
With software there are usually many solutions.
Model a desktop and two operations
•
In this example we model software that allows users to add and
remove icons from a desktop.
•
A
cut
operation removes one icon from the desktop.
•
A
paste
operation adds one icon to the desktop.
Problem Statement
•
Model a desktop, its icons, and cut and paste operations.
•
We will create two versions of the model:
•
Version #1: Hardcode the icons.
•
Version #2: Arbitrary set of icons.
Version #1: Simple Model
•
Let’s model a desktop that has just two icons named A and B, and a
cut operation that removes B.
A
B
Desktop (first)
A
Desktop (second)
cut
A set of Desktops, each with a set of icons
sig
Desktop {icons:
set
Icon
}
The
set
keyword means that
icons
maps each
Desktop
to a
set
of
Icon
(an
Icon
is either
A
or
B
).
Desktop0
Desktop0
Desktop1
A
B
A
icons
Desktop0 is mapped to this set: {A, B}Desktop1 is mapped to this (singleton) set: {A}Order the Desktops -- there is a first Desktop,
a second Desktop, etc.
open
util/ordering[Desktop]
“first” denotes the first Desktop. “first.icons”
denotes the icons on the first Desktop.
“prev” denotes the previous Desktop. Suppose d
denotes one of the Desktops, then d.prev.icons
denotes the icons on the previous Desktop.
“last” denotes the last Desktop.
“next” denotes the next Desktop.
There are two icons, A and B
abstract
sig
Icon {}one
sig
A
extends
Icon {}one
sig
B
extends
Icon {}enum
Icon { A, B }Alternatively:
Constrain the first desktop to contain both
icons, the second desktop to contain just A
fact
{first.icons = A + B
first.next.icons = A
}
S
p
e
c
i
f
y
i
n
t
h
e
r
u
n
c
o
m
m
a
n
d
t
h
a
t
t
h
e
i
n
s
t
a
n
c
e
i
s
t
o
c
o
n
t
a
i
n
2
D
e
s
k
t
o
p
s
.
run
{} for
3
but
2 Desktop
open
util/ordering[Desktop]
sig
Desktop {icons:
set
Icon
}
enum
Icon { A, B }fact
{first.icons = A + B
first.next.icons = A
}
run
{} for
3
but
2 Desktop
Version #2: Arbitrary icons, cut/paste
operations
•
We want the model to represent any set of icons on the first Desktop.
•
Let d = the first Desktop and i = an icon on the first Desktop.
The second Desktop = d - i, or
The second Desktop = d + j (where j is an icon not on d)
•
Let d = the second Desktop and i = an icon on the second Desktop.
The third Desktop = d - i, or
The third Desktop = d + j (where j is an icon not on d)
•
And so forth.
Here is one of the instances that Alloy
generated:
icon2
Desktop0
Desktop1
cut
icon3
Desktop2
paste
icon3
icon1
icon3
Desktop3
icon3
icon1
icon0
paste
Desktop4
cut
icon3
icon1
Desktop signature is same as before
open
util/ordering[Desktop]
sig
Desktop {icons:
set
Icon
}
Instead of enumerating the icons, have a set
of icons:
sig
Icon {}The first Desktop contains a set of icons:
fact
init {some
i:
set
Icon | first.icons = i
}
A Desktop cannot hold just any set of icons, a
Desktop is derived from its previous Desktop:
it has the icons on the previous Desktop, plus
or minus one icon
fact
Desktops_through_cut_and_paste {all
d: Desktop - first |
(
some
i: d.prev.icons | d.icons = d.prev.icons - i)
or
(
some
i: Icon - d.prev.icons | d.icons = d.prev.icons + i)
}
open
util/ordering[Desktop]
sig
Desktop {icons:
set
Icon
}
sig
Icon {}fact
init {some
i:
set
Icon | first.icons = i
}
fact
Desktops_through_cut_and_paste {all
d: Desktop - first |
(
some
i: d.prev.icons | d.icons = d.prev.icons - i)
or
(
some
i: Icon - d.prev.icons | d.icons = d.prev.icons + i)
}
run
{}for
5
Do Lab3
Explore the process of modeling desktops and software operations, including adding, removing, cutting, and pasting icons. Learn about creating versions of models with hardcoded icons or arbitrary sets. Dive into the ordering of desktops and the utilization of icons A and B in the model.
Uploaded on Oct 03, 2024 | 0 Views
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Desktop model Desktop0 Desktop2 Desktop1 cut paste icon1 icon3 icon2 icon3 icon3 Roger L. Costello March 24, 2018
Its time to model software In the previous examples there was just one or a small number of solutions (instances) satisfying the constraints. With software there are usually many solutions.
Model a desktop and two operations In this example we model software that allows users to add and remove icons from a desktop. A cut operation removes one icon from the desktop. A paste operation adds one icon to the desktop.
Problem Statement Model a desktop, its icons, and cut and paste operations. We will create two versions of the model: Version #1: Hardcode the icons. Version #2: Arbitrary set of icons.
Version #1: Simple Model Let s model a desktop that has just two icons named A and B, and a cut operation that removes B. Desktop (first) Desktop (second) cut A B A
A set of Desktops, each with a set of icons sig Desktop { icons: set Icon } The set keyword means that icons maps each Desktop to a set of Icon (an Icon is either A or B). icons Desktop0 A Desktop0 is mapped to this set: {A, B} Desktop0 B Desktop1 Desktop1 is mapped to this (singleton) set: {A} A
Order the Desktops -- there is a first Desktop, a second Desktop, etc. open util/ordering[Desktop] first denotes the first Desktop. first.icons denotes the icons on the first Desktop. prev denotes the previous Desktop. Suppose d denotes one of the Desktops, then d.prev.icons denotes the icons on the previous Desktop. last denotes the last Desktop. next denotes the next Desktop.
There are two icons, A and B abstractsig Icon {} onesig A extends Icon {} onesig B extends Icon {} Alternatively: enum Icon { A, B }
Constrain the first desktop to contain both icons, the second desktop to contain just A fact { first.icons = A + B first.next.icons = A }
Specify in the run is to contain 2 Desktops. run command that the instance run {} for 3 but 2 Desktop
open util/ordering[Desktop] sig Desktop { icons: set Icon } enum Icon { A, B } fact { first.icons = A + B first.next.icons = A } run {} for 3 but 2 Desktop
Version #2: Arbitrary icons, cut/paste operations We want the model to represent any set of icons on the first Desktop. Let d = the first Desktop and i = an icon on the first Desktop. The second Desktop = d - i, or The second Desktop = d + j (where j is an icon not on d) Let d = the second Desktop and i = an icon on the second Desktop. The third Desktop = d - i, or The third Desktop = d + j (where j is an icon not on d) And so forth.
Here is one of the instances that Alloy generated: Desktop0 Desktop2 Desktop1 cut paste icon1 icon3 icon2 icon3 icon3 paste Desktop3 Desktop4 cut icon0 icon1 icon1 icon3 icon3
Desktop signature is same as before open util/ordering[Desktop] sig Desktop { icons: set Icon }
Instead of enumerating the icons, have a set of icons: sig Icon {}
The first Desktop contains a set of icons: fact init { some i: set Icon | first.icons = i }
A Desktop cannot hold just any set of icons, a Desktop is derived from its previous Desktop: it has the icons on the previous Desktop, plus or minus one icon fact Desktops_through_cut_and_paste { all d: Desktop - first | (some i: d.prev.icons | d.icons = d.prev.icons - i) or (some i: Icon - d.prev.icons | d.icons = d.prev.icons + i) }
open util/ordering[Desktop] sig Desktop { icons: set Icon } sig Icon {} fact init { some i: set Icon | first.icons = i } fact Desktops_through_cut_and_paste { all d: Desktop - first | (some i: d.prev.icons | d.icons = d.prev.icons - i) or (some i: Icon - d.prev.icons | d.icons = d.prev.icons + i) } Do Lab3 run {} for 5
