ColoredFiles1.md

app: ColoredFiles1

• types:
  • a set of Files
  • a set of Colors
• concepts:
  • one Trash[File] named T
  • one Label[File,Color] named L
• views:
  • colors = L.labels
• invariants:
  • Only accessible files can be labeled with colors.
• reactions:

reaction delete_clear
when
	T.delete[f]
where
	some f.colors
then
	L.clear[f]

reaction affix_error
when
	L.affix[f,c]
where
	f not in T.accessible
then
	error

• formalizations: Alloy, TLA+