Continue working on the Alloy blog post

code/dyno-alloy/DynoAlloy.als

@@ -59,7 +59,7 @@ pred addBitfieldFlagNeg[b1: Bitfield, b2: Bitfield, flag: Flag] {
 
 enum Property { PMethod, PField, PPublic }
 
-sig Props {
+sig Symbol {
     properties: set Property
 }
 
@@ -69,11 +69,46 @@ pred flagMatchesPropery[flag: Flag, property: Property] {
     (flag = Public and property = PPublic)
 }
 
-pred bitfieldMatchesProperties[bitfield: Bitfield, props: Props] {
-    // All positive flags must be satisifed
-    all flag: bitfield.positiveFlags | some property: props.properties | flagMatchesPropery[flag, property]
-    // All negative flags must not be satisfied
-    all flag: bitfield.negativeFlags | no property: props.properties | flagMatchesPropery[flag, property]
+pred bitfieldMatchesProperties[bitfield: Bitfield, symbol: Symbol] {
+    all flag: bitfield.positiveFlags | some property: symbol.properties | flagMatchesPropery[flag, property]
+    all flag: bitfield.negativeFlags | no property: symbol.properties | flagMatchesPropery[flag, property]
+}
+
+bitfieldExists: run {
+    some Bitfield
+}
+
+matchingBitfieldExists: run {
+    some bitfield : Bitfield, symbol : Symbol | bitfieldMatchesProperties[bitfield, symbol]
+}
+
+matchingBitfieldExists2: run {
+    some bitfield : Bitfield, symbol : Symbol {
+        #bitfield.positiveFlags = 1
+        #bitfield.negativeFlags = 1
+        #symbol.properties = 2
+        bitfieldMatchesProperties[bitfield, symbol]
+    }
+}
+
+fact "method and field are incompatible" {
+    always no symbol: Symbol | {
+        PMethod in symbol.properties and PField in symbol.properties
+    }
+}
+
+fact "public and field are incompatible" {
+    always no symbol: Symbol | {
+        PPublic in symbol.properties and PField in symbol.properties
+    }
+}
+
+matchingBitfieldExists3: run {
+    some bitfield : Bitfield, symbol : Symbol {
+        #bitfield.positiveFlags = 2
+        #symbol.properties = 2
+        bitfieldMatchesProperties[bitfield, symbol]
+    }
 }
 
 pred configureState[filterState: FilterState] {
@@ -141,7 +176,7 @@ fact step {
 example: run {
     all searchState: SearchState {
         // a way that subsequent results of searching it will miss things.
-        eventually some props: Props, fs: FilterState, fsBroken: FilterState, exclude: Bitfield {
+        eventually some symbol: Symbol, fs: FilterState, fsBroken: FilterState, exclude: Bitfield {
             // Some search (fs) will cause a transition / modification of the search state...
             configureState[fs]
             updateOrSet[searchState.found, fs]
@@ -149,15 +184,15 @@ example: run {
             configureState[fsBroken]
             excludeBitfield[searchState.found', exclude]
 
-            // Will allow for a set of properties...
+            // Will allow for a symbol ...
             // ... that are left out of the original search...
-            not bitfieldMatchesProperties[searchState.found, props]
+            not bitfieldMatchesProperties[searchState.found, symbol]
             // ... and out of the current search
-            not (bitfieldMatchesProperties[fs.include, props] and not bitfieldMatchesProperties[searchState.found, props])
+            not (bitfieldMatchesProperties[fs.include, symbol] and not bitfieldMatchesProperties[searchState.found, symbol])
             // But would be matched by the broken search...
-            bitfieldMatchesProperties[fsBroken.include, props]
+            bitfieldMatchesProperties[fsBroken.include, symbol]
             // ... to not be matched by a search with the new state:
-            not (bitfieldMatchesProperties[fsBroken.include, props] and not bitfieldMatchesProperties[exclude, props])
+            not (bitfieldMatchesProperties[fsBroken.include, symbol] and not bitfieldMatchesProperties[exclude, symbol])
         }
     }
 }