Predicates &
Functions
Predicates
A predicate is a logical statement that is either true or
false.
• It's a fundamental concept in logic and mathematics, and
it is also used in various fields like computer science,
philosophy, and linguistics.
• In simpler terms, a predicate is a condition or property that
can be applied to something.
• For example, consider the statement "The cat is on the
mat." Here, "is on the mat" is a predicate that can be
applied to the subject "cat."
Predicates
In formal logic:
• A predicate is often represented by a symbol, like P(x).
• The variable x is called the argument of the predicate.
• The truth value of the predicate depends on the specific
value assigned to x.
Example:
Let's say we have a predicate IsEven(x). This predicate is
true if the number x is even, and false otherwise.
• IsEven(2) is true.
• IsEven(3) is false.
Predicates
Predicates in Programming:
Predicates are also commonly used in
programming languages, particularly in
functional programming. They can be used to
filter data, define conditions, and create more
expressive and concise code.
Predicates
In summary:
•A predicate is a statement that can be either
true or false.
•It often involves a subject and a property or
condition.
•Predicates are used in various fields, including
logic, mathematics, and computer science.
•In programming, predicates can be used to
define conditions, filter data, and create more
expressive code.
Predicates in Alloy Models
• Alloy models can have:
• Signatures
• Relations
• Multiplicity Constraints
• Facts
• Assertions
• Predicates
• Functions
•…
Predicate
• A predicate is like a programming
function that returns a Boolean.
• While they are a special case of Alloy
functions, they are more fundamental to
modeling and addressed first.
• Predicates take the form
pred name { constraint }
Ref. https://alloy.readthedocs.io/en/latest/language/predicates-and-functions.html#predicates
Predicates
• Once defined, predicates can be used as
part of Boolean expressions.
Predicates with Arguments
• Predicates can also take arguments
pred foo[a: Set1, b: Set2...] { expr }
• The initial argument to a predicate can be
passed in via a . join.
• The following two are equivalent:
pred[x, y, z]
x.pred[y, z]
Predicates General Form
Defines a predicate, with the
given name and (possibly
empty) parameters.
pred Name [parameters] {f}
A predicate always produces true
or false, so no type is needed.
The result is defined by the
formula f, which may reference
the parameters.
River Crossing Model
A farmer is on one shore of a river and has with him a fox,
a chicken, and a sack of grain. He has a boat that fits one
object besides himself. In the presence of the farmer nothing
gets eaten, but if left without the farmer, the fox will eat the
chicken, and the chicken will eat the grain. How can the
farmer get all three possessions across the river safely?
River Crossing Model
we define a signature Object, which represents the set of the
Farmer and his possessions. We partition the Object set into four
singleton subsets: Farmer, Fox, Chicken, and Grain.
River Crossing Model
The fox will eat the chicken if the farmer is not with them, and the
chicken will eat the grain if the farmer is not with them. We represent
this relationship with the eats relation from Object to Object, and we
constrain the exact value of the eats relation using the following fact:
River Crossing Model
We then create a signature called State, which represents the set of states
in our model. In each state, there are a certain set of objects on the near side
of the river, and a certain set on the far side of the river.
River Crossing Model
We would now like to say that all the Objects are on the near side
of the river in the first state.
We would also like to ask Alloy to find a solution in which all the
objects are on the far side of the river in the last state.
The problem is we do not yet have a way of talking about the
first state, the last state, or the fact that one may come before or
after another.
In sum, we need a way to construct a linear ordering of states and
refer to properties of that ordering.
Luckily, Alloy comes with a polymorphic linear ordering module
that can do that work for us.
River Crossing Model
• We import this module by adding the following line to the
beginning of our model.
• We parametarize on State, so now we can call order
comparison operations on elements of the State signature.
util/ordering
• The util/ordering module imposes a total ordering on the
atoms of State, and provides a few useful functions you
can use, including first, next, and last.
• first returns the first State atom in the linear ordering.
• last returns the last State atom in the linear ordering.
• next maps each State atom (except the last atom) to
the next State atom.
River Crossing Model
Now that we've loaded util/ordering, this is how we can use
the util/ordering module to say all the Objects are on the near side
of the river and none are on the far side in the initial state:
River Crossing Model
At any state, we will call the side of the river the farmer is currently
on the 'from' side and the other side the 'to' side. So our function
will stipulate how the set of objects on the 'from' and 'to' sides
change from state to state. Thus, we have the following signature for
our transition function:
pred crossRiver [from, from', to, to': set Object] { . . . }
River Crossing Model
• We know the farmer can take at most one object with him across
the river. We use "one x: from" to pick exactly one item from
the from set. There are two possibilities here:
• If x is not Farmer, then the predicate says that both the Farmer and x travel
from from to to, and if there were objects that would eat each other when left
alone then the eating happens.
• If x is Farmer, then the predicate says the Farmer travels alone from from to to,
and if there were objects that would eat each other when left alone then the eating
happens.
River Crossing Model
Next we must constrain each consecutive pair of States to abide by the
transition function. If the farmer is on the near side of the river, then the
near side of the river is the 'from' side and the far side of the river is the 'to'
side. And if the farmer is on the far side, then the far side is 'from' and the
near side 'to'. We express this constraint in the following Alloy fact.
The function next in the above fact is provided by
the util/ordering module. It returns the state that follows its argument in
the linear ordering. That is, s.next returns the state immediately
following s; unless s is the last state in the linear order, in which case it
returns the empty set. So the quantifying expression "all s: State, s':
s.next" effectively says "for all consecutive pairs of states". It is
equivalent to writing "all s, s': State | s' = s.next => ...".
Now that our state machine is
defined, we must ask Alloy to
produce a trace of the state
machine in which all the objects
are on the far side of the river in
the final state. To do so, we ask
Alloy to find a solution where at
the last State, we see every
Object is at the far side:
run { last.far = Object }
Recall that Object is just a set
and can be read as "the set of all
Objects". That is, we are saying
that, in the last State, the set of
things on the far shore equals the
set of all things.
• Without specifying a scope, Alloy will assume there are 3 atoms
of everything unless specified otherwise.
• In this case, Alloy will assume there are 3 State atoms.
• But Alloy Analyzer knows that there are exactly 4 Objects since
it is already defined to be the union of 4 singleton disjoint atoms
Farmer, Chicken, Fox, and Grain.
• Not surprisingly, Alloy finds no solutions, because the problem
can't be solved in only three states.
• If we steadily increase the scope on the set of States, we
eventually reach a point at which Alloy can find a solution at a
scope of 8.
• Thus, the command that finds the smallest solution to this
puzzle is
run { last.far = Object } for exactly 8 State
Instance
Functions
• Alloy functions have the same structure as
predicates but also return a value.
• Unlike functions in programming languages,
they are always executed within an
execution run, so their results are available
in the visualisation and the evaluator even if
you haven’t called them directly.
• This is very useful for some visualisations,
although the supporting code can be
disorienting when transitioning from
“regular” programming languages.
Functions General Form
fun Name [parameters] : type {e}
Defines a function, with the given name and (possibly
empty) parameters, and producing a relation (or set, or scalar)
of the given type.
The result is defined by the expression e, which may reference
the parameters.
Example
Running Scenarios
Example
Functions, Predicates
