Alloy - Revision history

David Geleßus: Add updated syntax overview (from prob2-doc, originally added by Joshua Schmidt)

2021-02-03T17:10:52Z

Add updated syntax overview (from prob2-doc, originally added by Joshua Schmidt)

← Older revision		Revision as of 17:10, 3 February 2021
Line 246:		Line 246:
	one DECL \| P existential quantification with exactly one solution		one DECL \| P existential quantification with exactly one solution
	lone DECL \| P quantification with one or zero solutions		lone DECL \| P quantification with one or zero solutions

	where the DECL follow the following form:		where the DECL follow the following form:
	x : S choose a singleton subset of S (like x : one S)		x : S choose a singleton subset of S (like x : one S)
	x : one S choose a singleton subset of S		x : one S choose a singleton subset of S
Line 264:		Line 264:
	S & T set intersection		S & T set intersection
	S - T set difference		S - T set difference
	# S cardinality of set		# S cardinality of set

	Set Predicates:		Set Predicates:
Line 277:		Line 277:
	{x:S \| P} set comprehension		{x:S \| P} set comprehension
	{DECL \| P} set comprehension, DECL has same format as for quantifiers		{DECL \| P} set comprehension, DECL has same format as for quantifiers
	let s : S \| P identifier definition		let s : S \| P identifier definition

	Relation Expressions:		Relation Expressions:
Line 289:		Line 289:
	^R transitive closure of binary relation		^R transitive closure of binary relation
	*R reflexive and transitive closure		*R reflexive and transitive closure

	Multiplicity Declarations:		Multiplicity Declarations:
	---------------------------		---------------------------
	The following multiplicity annotations are supported for binary (sub)-relations:		The following multiplicity annotations are supported for binary (sub)-relations:

	f in S -> T f is any relation from S to T (subset of cartesian product)		f in S -> T f is any relation from S to T (subset of cartesian product)
	f in S -> lone T f is a partial function from S to T		f in S -> lone T f is a partial function from S to T
	f in S -> one T f is a total function from S to T		f in S -> one T f is a total function from S to T
	f in S -> some T f is a total relation from S to T		f in S -> some T f is a total relation from S to T
	f in S one -> one T f is a total bijection from S to T		f in S one -> one T f is a total bijection from S to T
	f in S lone -> lone T f is a partial injection from S to T		f in S lone -> lone T f is a partial injection from S to T
	f in S lone -> one T f is a total injection from S to T		f in S lone -> one T f is a total injection from S to T
	f in S some -> lone T f is a partial surjection from S to T		f in S some -> lone T f is a partial surjection from S to T
	f in S some -> one T f is a total surjection from S to T		f in S some -> one T f is a total surjection from S to T
	f in S some -> T f is a surjective relation from S to T		f in S some -> T f is a surjective relation from S to T
	f in S some -> some T f is a total surjective relation from S to T		f in S some -> some T f is a total surjective relation from S to T

	Ordered Signatures:		Ordered Signatures:
Line 311:		Line 311:
	open util/ordering [S] as s		open util/ordering [S] as s

	s/first first element		s/first first element
	s/last last element		s/last last element
	s/next[s2] element after s2		s/max returns the largest element in s or the empty set
	s/nexts[s2] all elements after s2		s/min returns the smallest element in s or the empty set
	s/prev[s2] element before s2		s/next[s2] element after s2
	s/prevs[s2] all elements before s2		s/nexts[s2] all elements after s2
			s/prev[s2] element before s2
			s/prevs[s2] all elements before s2
			s/smaller[e1,e2] return the element with the smaller index
			s/larger[e1,e2] returns the element with the larger index
			s/lt[e1,e2] true if index(e1) < index(e2)
			s/lte[s2] true if index(e1) =< index(e2)
			s/gt[s2] true if index(e1) > index(e2)
			s/gte[s2] true if index(e1) >= index(e2)

	Sequences:		Sequences:
	----------		----------
			The longest allowed sequence length (maxseq) is set in the scope of a run or check command using the 'seq' keyword.
			Otherwise, a default value is used.
			The elements of a sequence s are enumerated from 0 to #s-1.

			s : seq S ordered and indexed sequence
			#s the cardinality of s
			s.isEmpty true if s is empty
			s.hasDups true if s contains duplicate elements
			s.first head element
			s.last last element
			s.butlast s without its last element
			s.rest tail of the sequence
			s.inds the set {0,..,#s-1} if s is not empty, otherwise the empty set
			s.lastIdx #s-1 if s is not empty, otherwise the empty set
			s.afterLastIdx #s if s is smaller than maxseq, otherwise the empty set
			s.idxOf [x] the first index of the occurence of x in s, the empty set if x does not occur in s
			s.add[x] insert x at index position i
			s.indsOf[i] the set of indices where x occurs in s, the empty set if x does not occur in s
			s.delete[i] delete the element at index i
			s.lastIdxOf[x] the last index of the occurence of x in s, the empty set if x does not occur in s
			s.append[s2] concatenate s and s2, truncate the result if it contains more than maxseq elements
			s.insert[i,x] insert x at index position i, remove the last element if #s = maxseq
			s.setAt[i,x] replace the value at index position i with x
			s.subseq[i,j] the subsequence of s from indices i to j inclusively

	s : ~~seq S ordered and indexed sequence~~		[see http://alloy.lcs.mit.edu/alloy/documentation/quickguide/seq.html]
	s.~~first head element~~
	s.~~rest tail of the sequence~~
	s.~~idxOf [x] returns the first index of the occurence of x in s, returns the empty set if x does not occur in s~~
	s.~~insert[i,x~~] ~~returns a new sequence where x is inserted at index position i~~

	Arithmetic Expressions and Predicates:		Arithmetic Expressions and Predicates:
Line 363:		Line 391:
	check NAME		check NAME

	run NAME for x global scope of less or equal x		run NAME for x global scope of less or equal x
	run NAME for exactly x1 but x2 S global scope of x1 but less or equal x2 S		run NAME for exactly x1 but x2 S global scope of x1 but less or equal x2 S
	run NAME for x1 S1,...,xk Sk individual scopes for signatures S1,..,Sk		run NAME for x1 S1,...,xk Sk individual scopes for signatures S1,..,Sk
	run NAME for x Int specify the integer bitwidth (integer overflows might occur)		run NAME for x Int specify the integer bitwidth (integer overflows might occur)
			run NAME for x seq specify the longest allowed sequence length
	</pre>		</pre>

Michael Leuschel at 16:31, 27 January 2021

2021-01-27T16:31:45Z

← Older revision		Revision as of 16:31, 27 January 2021
Line 1:		Line 1:
	[[Category:User Manual]]		[[Category:User Manual]]

	As of version 1.8 ProB provides support to load [~~http~~://~~alloy~~.~~mit.edu/alloy/~~ Alloy] models.		As of version 1.8 ProB provides support to load [https://alloytools.org Alloy] models.
	The Alloy models are translated to B machines by a [https://github.com/hhu-stups/alloy2b Java frontend].		The Alloy models are translated to B machines by a [https://github.com/hhu-stups/alloy2b Java frontend].

Michael Leuschel at 08:09, 2 October 2018

2018-10-02T08:09:52Z

← Older revision		Revision as of 08:09, 2 October 2018
Line 51:		Line 51:

	<pre>		<pre>
	/~~@ generated~~ /		MACHINE alloytranslation
	~~MACHINE queens~~		SETS /* deferred */
	~~SETS queen_~~		queen
	~~CONSTANTS x_queen~~, ~~x__queen~~, ~~y_queen~~		CONCRETE_CONSTANTS
	~~DEFINITIONS~~		x,
	~~show_ ==~~ ~~1=1 ;~~		x_,
	~~SET_PREF_MAXINT == 15 ; SET_PREF_MININT == -16~~		y
			/* PROMOTED OPERATIONS
			run0 */
	PROPERTIES		PROPERTIES
	~~(!(q_, q__).({q_} <~~: ~~queen_~~ & ~~{q__} <~~: ~~(queen_~~ - ~~{q_}) =~~>		x : queen --> INTEGER
	(~~not((x_queen~~(q_) = ~~x_queen~~(~~q__)))~~) & (~~not((y_queen(q_~~) = ~~y_queen~~(~~q__))~~))		& x_ : queen --> INTEGER
	~~& (not~~(~~((x_queen(q_~~) ~~+ y_queen~~(~~q_)~~) = (~~x_queen(q__~~) ~~+ y_queen~~(~~q__~~)~~))))~~		& y : queen --> INTEGER
	& (~~not(((x__queen(q_) + y_queen(q_)~~) = (~~x__queen~~(~~q__~~) + ~~y_queen~~(~~q__)))))~~)) &		& !this.(this : queen => x(this) >= 1 & y(this) >= 1 & x(this) <= card(queen) & y(this) <=
	card(~~queen_~~) = 4 &		card(queen) & x_(this) >= 1 & x_(this) <= card(queen) & x_(this) = (card(queen) + 1) - x(this)
	~~/* from signature declaration */~~ !(~~this_~~).({~~this_~~} ~~<: queen_~~ =>		)
	((~~x_queen(this_~~) >= ~~1)) &~~ (~~(y_queen(this_~~) ~~>= 1~~))		& card(queen) = 4
	& ((~~x_queen(this_~~) <= ~~card~~(~~queen_)~~))		& !(q,q_).(q_ : queen - {q} => not(x(q) = x(q_)) & not(y(q) = y(q_)) & not(x(q) + y(q) = x(
	& ((~~y_queen~~(~~this_~~) <= ~~card~~(~~queen_~~)))		q_) + y(q_)) & not(x_(q) + y(q) = x_(q_) + y(q_)))
	& (~~(x__queen(this_) >= 1~~)) & ((~~x__queen(this_~~) ~~<= card~~(~~queen_)))~~		INITIALISATION
	~~& ((x__queen(this_~~) = (~~(card(queen_~~) + ~~1) - x_queen~~(~~this_~~)))~~)) &~~		skip
	~~x_queen : queen_ --> INT &~~
	~~x__queen : queen_ --> INT &~~
	~~y_queen : queen_ --> INT~~
	OPERATIONS		OPERATIONS
	~~run_show~~ = ~~PRE show_~~ THEN skip END		run0 =
			PRE
			card(queen) = 4
			& !(q,q_).(q_ : queen - {q} => not(x(q) = x(q_)) & not(y(q) = y(q_)) & not(x(q) + y(q)
			= x(q_) + y(q_)) & not(x_(q) + y(q) = x_(q_) + y(q_)))
			THEN
			skip
			END
			/* DEFINITIONS
			PREDICATE show; */
	END		END
	</pre>		</pre>

Michael Leuschel: /* Installation */

2018-10-02T08:04:07Z

Installation

← Older revision		Revision as of 08:04, 2 October 2018
Line 10:		Line 10:

	== Installation ==		== Installation ==
	Alloy2B is included ~~with the lastest nightly builds~~ of ProB.		Alloy2B is included as of version 1.8.2 of ProB.

	You can build it yourself:		You can build Alloy2B yourself:
	* Clone or download [https://github.com/hhu-stups/alloy2b Alloy2B project on Github].		* Clone or download [https://github.com/hhu-stups/alloy2b Alloy2B project on Github].
	* Make jar file (gradle build) and		* Make jar file (gradle build) and

Michael Leuschel: /* Alloy Syntax */

2018-10-02T07:53:29Z

Alloy Syntax

Show changes

Michael Leuschel at 10:34, 5 September 2018

2018-09-05T10:34:08Z

← Older revision		Revision as of 10:34, 5 September 2018
Line 212:		Line 212:

	[[File:AlloyAtelierB.png\|800px\|center]]		[[File:AlloyAtelierB.png\|800px\|center]]


			== Alloy Syntax ==

			<pre>
			Logical predicates:
			-------------------
			P and Q conjunction
			P or Q disjunction
			P implies Q implication
			P iff Q equivalence
			not P negation
			all x:S \| P universal quantification
			some x:S \| P existential quantification
			some disjoint x,y : S \| P

			Alternative syntax:
			P && Q conjunction
			P \|\| Q disjunction
			P => Q implication
			P <=> Q equivalence
			! P negation

			Set Expressions:
			----------------
			univ all objects
			none empty set
			S + T set union
			S & T set intersection
			S - T set difference
			# S cardinality of set

			Set Predicates:
			---------------
			no S set S is empty
			S in T R is subset of S
			S = T set equality
			some S set S is not empty
			one S S is singleton set
			lone S S is empty or a singleton

			Relation Expressions:
			----------------------
			R -> S Cartesian product
			R . S relational join
			S <: R domain restriction of relation R for unary set S
			R :> S range restriction of relation R for unary set S
			~R relational inverse
			^R transitive closure of binary relation
			*R reflexive and transitive closure

			Arithmetic Expressions and Predicates:
			--------------------------------------
			You need to open util/integer:

			plus[X,Y] addition
			minus[X,Y] subtraction
			mul[X,Y] multiplication
			div[X,Y] division
			rem[X,Y] remainder
			sum[S] sum of integers of set S

			X < Y less
			X = Y integer equality
			X > Y greater
			X =< Y less or equal
			X >= Y greater or equal
			</pre>

Sebastian Krings: /* Installation */

2018-02-09T13:09:27Z

Installation

← Older revision		Revision as of 13:09, 9 February 2018
Line 10:		Line 10:

	== Installation ==		== Installation ==
			Alloy2B is included with the lastest nightly builds of ProB.

	Clone or download [https://github.com/hhu-stups/alloy2b Alloy2B project on Github].		You can build it yourself:
	Make jar file (gradle build) and put resulting alloy2b-*.jar file into ProB's lib folder.		* Clone or download [https://github.com/hhu-stups/alloy2b Alloy2B project on Github].
			* Make jar file (gradle build) and
			* put resulting alloy2b-*.jar file into ProB's lib folder.

	== Examples ==		== Examples ==

Michael Leuschel: /* Examples */

2018-02-07T11:23:21Z

Examples

← Older revision		Revision as of 11:23, 7 February 2018
Line 205:		Line 205:
	END		END
	</pre>		</pre>

			The following shows AtelierB proving the above assertion:

			[[File:AlloyAtelierB.png\|800px\|center]]

Michael Leuschel: /* Examples */

2018-02-07T11:17:29Z

Examples

@@ Line 72: / Line 72: @@
 OPERATIONS
      run_show = PRE show_ THEN skip END
 END
 </pre>

Michael Leuschel: /* N-Queens */

2018-02-07T08:26:32Z

N-Queens

← Older revision		Revision as of 08:26, 7 February 2018
Line 41:		Line 41:

	This can be loaded in ProB, as shown in the following screenshot.		This can be loaded in ProB, as shown in the following screenshot.
	To run the "show" command you have to use "Find Sequence..." command in the "Constraint-Based Checking" submenu of the "Verify" menu.		To run the "show" command you have to use "Find Sequence..." command for "run_show" in the "Constraint-Based Checking" submenu of the "Verify" menu.
	[[File:ProBAlloyQueens.png\|800px\|center]]		[[File:ProBAlloyQueens.png\|800px\|center]]