New keyword 'then' as synonym for ','

1

Alloy often has two notations for operators i.e. and/&&. Some people prefer the more verbose notation.
I propose to introduce the operator “then” as a synonym for “,” the trace sequence operator.

I think in the code one has to add just one line in Alloy.lex

"then" { return alloy_sym(yytext(), CompSym.TRCSEQ );}

after line 234.

But one has to change documentation and It’s of course a question of the conceptual integrity of the language too. But imho it would fit.

–Burkhardt

2

This was a bug report so @grayswandyr, @DanielJackson @aleks and others please let us know what you think. Need a resolution on this. I’ve some time over the holidays so if there is a quick resolution I can do the update.

3

Hi,
I see the rationale. I don’t have a definite opinion on the matter so I’ll just list pros and cons:

  1. ; is litterally a low-precedence right-associative and after so we already have, by definition, a verbose notation (and after);
  2. on the other hand, low precedence with right-associativity is really the important bit here , so with and after the user must stack lots of parentheses and take care that they’re balanced, plus it’s not very readable.
  3. then may be confusing because it evokes an if/then/else (which, by the way, some users would be happy to have);
  4. it adds yet another keyword.

david

2 Likes
4

Hi,

agree with 3. Does anyone have a better and more appropriate term?

1 Like
5

Can you provide some motivation for introducing this new keyword, i.e., something more significant than “some people prefer the more verbose notation”?

For example, can you provide a snippet of Alloy that you think would look better or more readable using the then notation?

6

The motivation for introducing then came from the following example.

/* Specification of a concrete scenario for
   the echo algorithm in Alloy using the specification in module echo_var
*/

// the specification of the algorithm with transition predicates initiate and so on
open echo_var

// the concrete example of a graph
pred exampleGraph [N0, N1, N2, N3, N4, N5, N6: Node] {
	Node = N0 + N1 + N2 + N3 + N4 + N5 + N6
	neighbors = N0->N2 + N0->N3 + 
              N1->N2 + N1->N3 +
              N2->N0 + N2->N1 + N2->N3 + N2->N4 +
              N3->N0 + N3->N1 + N3->N2 + N3->N4 + N3->N5 +
              N4->N2 + N4->N3 + N4->N6 +
              N5->N3 + N5->N6 +
              N6->N4 + N6->N5
}

// an explicitly given scenario 
run Scenario {
	some disj N0, N1, N2, N3, N4, N5, N6: Node {
		exampleGraph[N0, N1, N2, N3, N4, N5, N6]
		
		initiate[N2];
		forward[N0, N2];
		forward[N4, N2];
		forward[N3, N4]; 
		forward[N1, N3]; 
		forward[N6, N4]; 
		forward[N5, N3]; 
		echo[N5]; 
		echo[N6];
		echo[N1];
		echo[N3];
		echo[N4];
		echo[N0];
		echo[N2];
		always stutter
	}
} for 7 Node, 15 steps

Someone who’s first programming language was C (as in my case) or Java (as in my students case) seeing a semicolon ; thinks of a sequence of assignments and statements, not of a sequence of states. So I thaught, that something like this would better express what we mean:

   initiate[N2]
   then forward[N0, N2]
   then 
   ...
   then echo[N2]
   then always stutter

But I agree, it’s a minor point.

Kind regards
Burkhardt

7

Notice that it doesn’t have to be states. Supposing you model events (call them ev_i) using the reified-event idiom, you may describe a sequence of “instructions” (that is, events):

run { some ev_1; some ev_3; some ev_7 }
8

I should have formulated more precisely: I would like the so-called “instructions” to be understood as specifications of a sequence of state transitions. That’s the case in David’s example too, isn’t it?