Update Alloy DSL for Alloy 6

pygments/lexers/dsls.py

@@ -601,8 +601,9 @@ class AlloyLexer(RegexLexer):
 
     flags = re.MULTILINE | re.DOTALL
 
-    iden_rex = r'[a-zA-Z_][\w\']*'
-    text_tuple = (r'[^\S\n]+', Whitespace)
+    iden_rex = r'[a-zA-Z_][\w]*"*'
+    string_rex = r'"\b(\\\\|\\[^\\]|[^"\\])*"'
+    text_tuple = (r'[^\S\n]+', Text)
 
     tokens = {
         'sig': [
@@ -621,6 +622,10 @@ class AlloyLexer(RegexLexer):
             (r'\{', Operator, '#pop'),
             (iden_rex, Name, '#pop'),
         ],
+        'fact': [
+            include('fun'),
+            (string_rex, String, '#pop')
+        ],
         'root': [
             (r'--.*?$', Comment.Single),
             (r'//.*?$', Comment.Single),
@@ -631,18 +636,21 @@ class AlloyLexer(RegexLexer):
             (r'(sig|enum)(\s+)', bygroups(Keyword.Declaration, Whitespace), 'sig'),
             (r'(iden|univ|none)\b', Keyword.Constant),
             (r'(int|Int)\b', Keyword.Type),
-            (r'(this|abstract|extends|set|seq|one|lone|let)\b', Keyword),
+            (r'(var|this|abstract|extends|set|seq|one|lone|let)\b', Keyword),
             (r'(all|some|no|sum|disj|when|else)\b', Keyword),
-            (r'(run|check|for|but|exactly|expect|as)\b', Keyword),
+            (r'(run|check|for|but|exactly|expect|as|steps)\b', Keyword),
+            (r'(always|after|eventually|until|release)\b', Keyword), # future time operators
+            (r'(historically|before|once|since|triggered)\b', Keyword), # past time operators
             (r'(and|or|implies|iff|in)\b', Operator.Word),
-            (r'(fun|pred|fact|assert)(\s+)', bygroups(Keyword, Whitespace), 'fun'),
-            (r'!|#|&&|\+\+|<<|>>|>=|<=>|<=|\.|->', Operator),
-            (r'[-+/*%=<>&!^|~{}\[\]().]', Operator),
+            (r'(fun|pred|assert)(\s+)', bygroups(Keyword, Text), 'fun'),
+            (r'(fact)(\s+)', bygroups(Keyword, Text), 'fact'),
+            (r'!|#|&&|\+\+|<<|>>|>=|<=>|<=|\.\.|\.|->', Operator),
+            (r'[-+/*%=<>&!^|~{}\[\]().\';]', Operator),
             (iden_rex, Name),
             (r'[:,]', Punctuation),
             (r'[0-9]+', Number.Integer),
-            (r'"(\\\\|\\[^\\]|[^"\\])*"', String),
-            (r'\n', Whitespace),
+            (string_rex, String),
+            (r'\n', Text),
         ]
     }
 

tests/examplefiles/alloy/example.als

@@ -32,8 +32,8 @@ module examples/systems/views
  *
  * As a terminological convention, when there are two
  * complementary view relationships, we will give them types
- * t and t'. For example, KeySetView propagates from map to
- * set, and KeySetView' propagates from set to map.
+ * t and t". For example, KeySetView propagates from map to
+ * set, and KeySetView" propagates from set to map.
  *
  * author: Daniel Jackson
  */
@@ -76,12 +76,12 @@ sig SetRef extends Ref {}
 fact {State.obj[SetRef] in Set}
 
 abstract sig ViewType {}
-one sig KeySetView, KeySetView', IteratorView extends ViewType {}
+one sig KeySetView, KeySetView", IteratorView extends ViewType {}
 fact ViewTypes {
   State.views[KeySetView] in MapRef -> SetRef
-  State.views[KeySetView'] in SetRef -> MapRef
+  State.views[KeySetView"] in SetRef -> MapRef
   State.views[IteratorView] in IteratorRef -> SetRef
-  all s: State | s.views[KeySetView] = ~(s.views[KeySetView'])
+  all s: State | s.views[KeySetView] = ~(s.views[KeySetView"])
   }
 
 /**
@@ -107,20 +107,20 @@ pred allocates [pre, post: State, rs: set Ref] {
   }
 
 /** 
- * models frame condition that limits change to view object from v to v' when backing object changes to b'
+ * models frame condition that limits change to view object from v to v" when backing object changes to b"
  */
-pred viewFrame [t: ViewType, v, v', b': Object] {
-  t in KeySetView => v'.elts = dom [b'.map]
-  t in KeySetView' => b'.elts = dom [v'.map]
-  t in KeySetView' => (b'.elts) <: (v.map) = (b'.elts) <: (v'.map)
-  t in IteratorView => v'.elts = b'.left + b'.done
+pred viewFrame [t: ViewType, v, v", b": Object] {
+  t in KeySetView => v".elts = dom [b".map]
+  t in KeySetView" => b".elts = dom [v".map]
+  t in KeySetView" => (b".elts) <: (v.map) = (b".elts) <: (v".map)
+  t in IteratorView => v".elts = b".left + b".done
   }
 
 pred MapRef.keySet [pre, post: State, setRefs: SetRef] {
   post.obj[setRefs].elts = dom [pre.obj[this].map]
   modifies [pre, post, none]
   allocates [pre, post, setRefs]
-  post.views = pre.views + KeySetView->this->setRefs + KeySetView'->setRefs->this
+  post.views = pre.views + KeySetView->this->setRefs + KeySetView"->setRefs->this
   }
 
 pred MapRef.put [pre, post: State, k, v: Ref] {
@@ -141,22 +141,22 @@ pred SetRef.iterator [pre, post: State, iterRef: IteratorRef] {
   }
 
 pred IteratorRef.remove [pre, post: State] {
-  let i = pre.obj[this], i' = post.obj[this] {
-    i'.left = i.left
-    i'.done = i.done - i.lastRef
-    no i'.lastRef
+  let i = pre.obj[this], i" = post.obj[this] {
+    i".left = i.left
+    i".done = i.done - i.lastRef
+    no i".lastRef
     }
   modifies [pre,post,this]
   allocates [pre, post, none]
   pre.views = post.views
   }
 
 pred IteratorRef.next [pre, post: State, ref: Ref] {
-  let i = pre.obj[this], i' = post.obj[this] {
+  let i = pre.obj[this], i" = post.obj[this] {
     ref in i.left
-    i'.left = i.left - ref
-    i'.done = i.done + ref
-    i'.lastRef = ref
+    i".left = i.left - ref
+    i".done = i.done + ref
+    i".lastRef = ref
     }
   modifies [pre, post, this]
   allocates [pre, post, none]