permissions-model.thm

<?xml version="1.0"?>
<alloy>

<view>

<defaultnode/>

<defaultedge/>

<node>
   <type name="App"/>
   <type name="CannotSee"/>
   <type name="Edit"/>
   <type name="Int"/>
   <type name="Own"/>
   <type name="String"/>
   <type name="Stutter"/>
   <type name="univ"/>
   <type name="Use"/>
   <type name="open$4/Ord"/>
   <type name="ordering/Ord"/>
   <type name="seq/Int"/>
   <set name="$user_self_grants_own_access_o" type="Object"/>
</node>

<node color="Blue">
   <type name="Object"/>
</node>

<node color="Gray">
   <type name="User"/>
</node>

<node hideunconnected="no">
   <type name="RootFolder"/>
</node>

<node hideunconnected="no" showlabel="no">
   <set name="$events" type="Event"/>
</node>

<node hideunconnected="yes" shape="Parallelogram" color="Red">
   <type name="Event"/>
</node>

<node shape="Egg" color="Green">
   <type name="Group"/>
</node>

<node shape="Ellipse">
   <type name="Folder"/>
</node>

<node style="Dashed" color="Blue">
   <type name="Move"/>
</node>

<node visible="no">
   <type name="Permission"/>
</node>

<node visible="no" showlabel="no">
   <set name="$stutter_happens" type="Event"/>
</node>

<edge constraint="no">
   <relation name="explicit"> <type name="Group"/> <type name="Permission"/> <type name="Object"/> </relation>
   <relation name="groups"> <type name="User"/> <type name="Group"/> </relation>
</edge>

<edge style="inherit">
   <relation name="children"> <type name="Folder"/> <type name="Object"/> </relation>
</edge>

<edge style="inherit" visible="no" attribute="yes" constraint="no">
   <relation name="calculated"> <type name="Group"/> <type name="Permission"/> <type name="Object"/> </relation>
   <relation name="calculated"> <type name="User"/> <type name="Permission"/> <type name="Object"/> </relation>
</edge>

<edge visible="no">
   <relation name="parent"> <type name="Object"/> <type name="Folder"/> </relation>
</edge>

<edge visible="no" attribute="yes" constraint="no" label="args">
   <relation name="$move_happens"> <type name="Event"/> <type name="Object"/> <type name="Folder"/> </relation>
</edge>

</view>

</alloy>