Commit 677e72bb3ef161edce1f8b9727f6ab5c6b5da0b7

Authored by Alcino Cunha
1 parent 0190bb751a
Exists in master

Alloy specifications updated with themes

README
... ... @@ -0,0 +1 @@
  1 +This repository contains artificats related to PTCRISync, the ORCID based synchronization protocol of PTCRIS.
0 2 \ No newline at end of file
... ...
specification/v0.3/ptcris_v3.als
... ... @@ -52,7 +52,7 @@ pred identical[w,w':Work] {
52 52  
53 53 // Defines similar Works that are considered grouped.
54 54 fun similar[r: ORCID] : Work -> Work {
55   - *{w1,w2 : r.works | some w1.uids & w2.uids} |
  55 + *{w1,w2 : r.works | some w1.uids & w2.uids}
56 56 }
57 57  
58 58 fun _similar[] : ORCID -> Work -> Work {
... ... @@ -678,7 +678,6 @@ pred EXPORTED_S4[p:PTCris,o:ORCID] {
678 678 run EXPORTED_S4 {some o:ORCID,o':o.next,p:PTCris,p':p.next |
679 679 EXPORTED_S4[p',o] && not EXPORTED[p',o] && IMPORTED[p',o] && EXPORT[o,o',p'] } for 20 but 2 ORCID, 2 PTCris
680 680  
681   -
682 681 pred SYNC_S1[p:PTCris,o:ORCID] {
683 682 p.productions = Production0+Production1
684 683 Production0.key = Key2 && Production0.metadata = Metadata2 && Production0.uids = EID0+DOI0+Handle1+DOI1
... ...
specification/v0.3/ptcris_v3.thm
... ... @@ -0,0 +1,175 @@
  1 +<?xml version="1.0"?>
  2 +<alloy>
  3 +
  4 +<view nodetheme="Martha" edgetheme="Martha">
  5 +
  6 +<projection> <type name="Repository"/> </projection>
  7 +
  8 +<defaultnode/>
  9 +
  10 +<defaultedge/>
  11 +
  12 +<node>
  13 + <type name="Int"/>
  14 + <type name="Key0"/>
  15 + <type name="Key1"/>
  16 + <type name="Key2"/>
  17 + <type name="Metadata0"/>
  18 + <type name="Metadata1"/>
  19 + <type name="Metadata2"/>
  20 + <type name="ORCID"/>
  21 + <type name="Production0"/>
  22 + <type name="Production1"/>
  23 + <type name="Production2"/>
  24 + <type name="PTCRIS"/>
  25 + <type name="PTCris"/>
  26 + <type name="Putcode0"/>
  27 + <type name="Putcode1"/>
  28 + <type name="Putcode2"/>
  29 + <type name="Putcode3"/>
  30 + <type name="Putcode4"/>
  31 + <type name="Repository"/>
  32 + <type name="Scopus"/>
  33 + <type name="univ"/>
  34 + <type name="User"/>
  35 + <type name="Work0"/>
  36 + <type name="Work1"/>
  37 + <type name="Work2"/>
  38 + <type name="Work3"/>
  39 + <type name="Work4"/>
  40 + <type name="Work5"/>
  41 + <type name="seq/Int"/>
  42 + <set name="$IMPORTED_S4_o" type="ORCID"/>
  43 + <set name="$IMPORTED_S4_o&apos;" type="ORCID"/>
  44 + <set name="$IMPORTED_S4_p" type="PTCris"/>
  45 + <set name="$IMPORTED_S4_p&apos;" type="PTCris"/>
  46 + <set name="First" type="open$3/Ord"/>
  47 + <set name="First" type="ordering/Ord"/>
  48 + <set name="Next" type="open$3/Ord"/>
  49 + <set name="Next" type="ordering/Ord"/>
  50 +</node>
  51 +
  52 +<node color="Green">
  53 + <type name="Work"/>
  54 +</node>
  55 +
  56 +<node color="Yellow">
  57 + <type name="Production"/>
  58 +</node>
  59 +
  60 +<node label="DOI0">
  61 + <type name="UID2"/>
  62 +</node>
  63 +
  64 +<node label="DOI1">
  65 + <type name="UID0"/>
  66 +</node>
  67 +
  68 +<node label="EID1">
  69 + <type name="UID1"/>
  70 +</node>
  71 +
  72 +<node label="Handle0">
  73 + <type name="UID4"/>
  74 +</node>
  75 +
  76 +<node label="Handle1">
  77 + <type name="UID3"/>
  78 +</node>
  79 +
  80 +<node shape="Box">
  81 + <type name="Creation"/>
  82 + <type name="Modification"/>
  83 +</node>
  84 +
  85 +<node showlabel="no">
  86 + <set name="$IMPORTED_S4_p1" type="Production0"/>
  87 + <set name="$IMPORTED_S4_pre_p1" type="Production0"/>
  88 + <set name="$IMPORTED_S4_pre_w1" type="Work0"/>
  89 + <set name="$IMPORTED_S4_pre_w2" type="Work1"/>
  90 + <set name="$IMPORTED_S4_pre_w3" type="Work2"/>
  91 + <set name="$IMPORTED_S4_pre_w4" type="Work3"/>
  92 + <set name="$IMPORTED_S4_w1" type="Work0"/>
  93 + <set name="$IMPORTED_S4_w3" type="Work2"/>
  94 + <set name="$IMPORTED_S4_w4" type="Work3"/>
  95 + <set name="productions" type="Production"/>
  96 + <set name="works" type="Work"/>
  97 +</node>
  98 +
  99 +<node showlabel="no" shape="Ellipse">
  100 + <set name="preferred" type="Work"/>
  101 +</node>
  102 +
  103 +<node showlabel="no" style="Bold">
  104 + <set name="exported" type="Production"/>
  105 +</node>
  106 +
  107 +<node visible="no">
  108 + <type name="Source"/>
  109 + <type name="String"/>
  110 + <type name="open$3/Ord"/>
  111 + <type name="open$4/Ord"/>
  112 + <type name="ordering/Ord"/>
  113 +</node>
  114 +
  115 +<node visible="no" color="Black">
  116 + <type name="UID"/>
  117 +</node>
  118 +
  119 +<node visible="no" shape="Box" color="Blue">
  120 + <type name="Metadata"/>
  121 +</node>
  122 +
  123 +<node visible="no" shape="Box" color="Gray">
  124 + <type name="Output"/>
  125 +</node>
  126 +
  127 +<node visible="no" shape="Hexagon" color="White">
  128 + <type name="Putcode"/>
  129 +</node>
  130 +
  131 +<node visible="no" shape="Hexagon" color="Yellow">
  132 + <type name="Notification"/>
  133 +</node>
  134 +
  135 +<node visible="no" shape="Parallelogram" color="Green">
  136 + <type name="Key"/>
  137 +</node>
  138 +
  139 +<node visible="yes" showlabel="no">
  140 + <set name="outputs" type="Output"/>
  141 +</node>
  142 +
  143 +<node visible="yes" showlabel="no" style="Dashed">
  144 + <set name="notifications" type="Notification"/>
  145 +</node>
  146 +
  147 +<edge color="Blue" style="Dashed" label="similar">
  148 + <relation name="$_similar"> <type name="Work"/> <type name="Work"/> </relation>
  149 +</edge>
  150 +
  151 +<edge color="Gray" constraint="no">
  152 + <relation name="Next"> <type name="open$4/Ord"/> <type name="Source"/> <type name="Source"/> </relation>
  153 +</edge>
  154 +
  155 +<edge color="Gray" visible="no" attribute="yes" constraint="no">
  156 + <relation name="First"> <type name="open$4/Ord"/> <type name="Source"/> </relation>
  157 + <relation name="source"> <type name="Work"/> <type name="Source"/> </relation>
  158 +</edge>
  159 +
  160 +<edge visible="no" attribute="yes">
  161 + <relation name="key"> <type name="Notification"/> <type name="Key"/> </relation>
  162 + <relation name="key"> <type name="Production"/> <type name="Key"/> </relation>
  163 + <relation name="metadata"> <type name="Creation"/> <type name="Metadata"/> </relation>
  164 + <relation name="metadata"> <type name="Production"/> <type name="Metadata"/> </relation>
  165 + <relation name="metadata"> <type name="Work"/> <type name="Metadata"/> </relation>
  166 + <relation name="putcode"> <type name="Work"/> <type name="Putcode"/> </relation>
  167 +</edge>
  168 +
  169 +<edge visible="no" attribute="yes" constraint="no">
  170 + <relation name="uids"> <type name="Output"/> <type name="UID"/> </relation>
  171 +</edge>
  172 +
  173 +</view>
  174 +
  175 +</alloy>
... ...
specification/v0.4/ptcris_v4.als
... ... @@ -709,7 +709,6 @@ pred EXPORTED_S4[p:PTCris,o:ORCID] {
709 709 run EXPORTED_S4 {some o:ORCID,o':o.next,p:PTCris,p':p.next |
710 710 EXPORTED_S4[p',o] && not EXPORTED[p',o] && IMPORTED[p',o] && EXPORT[o,o',p'] } for 20 but 2 ORCID, 2 PTCris, 5 Work
711 711  
712   -
713 712 pred SYNC_S1[p:PTCris,o:ORCID] {
714 713 p.productions = Production0+Production1
715 714 Production0.key = Key2 && Production0.metadata = Metadata2 && Production0.uids = EID0+DOI0+Handle1+DOI1
... ...
specification/v0.4/ptcris_v4.thm
... ... @@ -0,0 +1,199 @@
  1 +<?xml version="1.0"?>
  2 +<alloy>
  3 +
  4 +<view nodetheme="Martha" edgetheme="Martha">
  5 +
  6 +<projection> <type name="Repository"/> </projection>
  7 +
  8 +<defaultnode/>
  9 +
  10 +<defaultedge/>
  11 +
  12 +<node>
  13 + <type name="DOI0"/>
  14 + <type name="DOI1"/>
  15 + <type name="EID0"/>
  16 + <type name="EID1"/>
  17 + <type name="Group0"/>
  18 + <type name="Group1"/>
  19 + <type name="Group2"/>
  20 + <type name="Group3"/>
  21 + <type name="Group4"/>
  22 + <type name="Handle0"/>
  23 + <type name="Handle1"/>
  24 + <type name="Int"/>
  25 + <type name="ORCID"/>
  26 + <type name="Production0"/>
  27 + <type name="Production1"/>
  28 + <type name="Production2"/>
  29 + <type name="PTCRIS"/>
  30 + <type name="PTCris"/>
  31 + <type name="Repository"/>
  32 + <type name="Scopus"/>
  33 + <type name="univ"/>
  34 + <type name="User"/>
  35 + <type name="Work0"/>
  36 + <type name="Work1"/>
  37 + <type name="Work2"/>
  38 + <type name="Work3"/>
  39 + <type name="Work4"/>
  40 + <type name="Work5"/>
  41 + <type name="open$5/Ord"/>
  42 + <type name="seq/Int"/>
  43 + <set name="$EXPORTED_S4_o" type="ORCID"/>
  44 + <set name="$EXPORTED_S4_o&apos;" type="ORCID"/>
  45 + <set name="$EXPORTED_S4_p" type="PTCris"/>
  46 + <set name="$EXPORTED_S4_p&apos;" type="PTCris"/>
  47 + <set name="First" type="open$3/Ord"/>
  48 + <set name="First" type="ordering/Ord"/>
  49 + <set name="Next" type="open$3/Ord"/>
  50 + <set name="Next" type="ordering/Ord"/>
  51 +</node>
  52 +
  53 +<node color="Green">
  54 + <type name="Work"/>
  55 +</node>
  56 +
  57 +<node color="Yellow">
  58 + <type name="Production"/>
  59 +</node>
  60 +
  61 +<node label="K0">
  62 + <type name="Key0"/>
  63 +</node>
  64 +
  65 +<node label="K1">
  66 + <type name="Key1"/>
  67 +</node>
  68 +
  69 +<node label="K2">
  70 + <type name="Key2"/>
  71 +</node>
  72 +
  73 +<node label="MD0">
  74 + <type name="Metadata0"/>
  75 +</node>
  76 +
  77 +<node label="MD1">
  78 + <type name="Metadata1"/>
  79 +</node>
  80 +
  81 +<node label="MD2">
  82 + <type name="Metadata2"/>
  83 +</node>
  84 +
  85 +<node label="MD3">
  86 + <type name="Metadata3"/>
  87 +</node>
  88 +
  89 +<node label="PC0">
  90 + <type name="Putcode0"/>
  91 +</node>
  92 +
  93 +<node label="PC1">
  94 + <type name="Putcode1"/>
  95 +</node>
  96 +
  97 +<node label="PC2">
  98 + <type name="Putcode2"/>
  99 +</node>
  100 +
  101 +<node label="PC3">
  102 + <type name="Putcode3"/>
  103 +</node>
  104 +
  105 +<node label="PC4">
  106 + <type name="Putcode4"/>
  107 +</node>
  108 +
  109 +<node shape="Box">
  110 + <type name="Creation"/>
  111 + <type name="Modification"/>
  112 +</node>
  113 +
  114 +<node shape="Trapezoid">
  115 + <type name="Group"/>
  116 +</node>
  117 +
  118 +<node showlabel="no">
  119 + <set name="productions" type="Production"/>
  120 +</node>
  121 +
  122 +<node showlabel="no" style="Bold">
  123 + <set name="exported" type="Production"/>
  124 +</node>
  125 +
  126 +<node visible="no">
  127 + <type name="Source"/>
  128 + <type name="String"/>
  129 + <type name="open$3/Ord"/>
  130 + <type name="open$4/Ord"/>
  131 + <type name="ordering/Ord"/>
  132 +</node>
  133 +
  134 +<node visible="no" color="Black">
  135 + <type name="UID"/>
  136 +</node>
  137 +
  138 +<node visible="no" shape="Box" color="Blue">
  139 + <type name="Metadata"/>
  140 +</node>
  141 +
  142 +<node visible="no" shape="Box" color="Gray">
  143 + <type name="Output"/>
  144 +</node>
  145 +
  146 +<node visible="no" shape="Hexagon" color="White">
  147 + <type name="Putcode"/>
  148 +</node>
  149 +
  150 +<node visible="no" shape="Hexagon" color="Yellow">
  151 + <type name="Notification"/>
  152 +</node>
  153 +
  154 +<node visible="no" shape="Parallelogram" color="Green">
  155 + <type name="Key"/>
  156 +</node>
  157 +
  158 +<node visible="yes" showlabel="no">
  159 + <set name="$_works" type="Work"/>
  160 + <set name="groups" type="Group"/>
  161 + <set name="outputs" type="Output"/>
  162 +</node>
  163 +
  164 +<node visible="yes" showlabel="no" shape="Ellipse">
  165 + <set name="$_preferred" type="Work"/>
  166 +</node>
  167 +
  168 +<node visible="yes" showlabel="no" style="Dashed">
  169 + <set name="notifications" type="Notification"/>
  170 +</node>
  171 +
  172 +<edge color="Blue">
  173 + <relation name="works"> <type name="Group"/> <type name="Work"/> </relation>
  174 +</edge>
  175 +
  176 +<edge color="Gray" visible="no" attribute="yes" constraint="no">
  177 + <relation name="source"> <type name="Work"/> <type name="Source"/> </relation>
  178 +</edge>
  179 +
  180 +<edge visible="no" attribute="no" constraint="no">
  181 + <relation name="uids"> <type name="Output"/> <type name="UID"/> </relation>
  182 +</edge>
  183 +
  184 +<edge visible="no" attribute="yes">
  185 + <relation name="key"> <type name="Notification"/> <type name="Key"/> </relation>
  186 + <relation name="key"> <type name="Production"/> <type name="Key"/> </relation>
  187 + <relation name="metadata"> <type name="Creation"/> <type name="Metadata"/> </relation>
  188 + <relation name="metadata"> <type name="Production"/> <type name="Metadata"/> </relation>
  189 + <relation name="metadata"> <type name="Work"/> <type name="Metadata"/> </relation>
  190 + <relation name="putcode"> <type name="Work"/> <type name="Putcode"/> </relation>
  191 +</edge>
  192 +
  193 +<edge visible="no" attribute="yes" label="ids">
  194 + <relation name="$_uids"> <type name="Output"/> <type name="UID"/> </relation>
  195 +</edge>
  196 +
  197 +</view>
  198 +
  199 +</alloy>
... ...