Functional Modelling System

IngmarDasseville
3,956 views
undefined

Open Source Your Knowledge, Become a Contributor

Technology knowledge has to be shared and made accessible for free. Join the movement.

Create Content

First Steps: FMS as a calculator

Sums

Let's see how we can use FMS as a calculator. We can define an identifier like x to be a numeric value like 4+5 as: x := 4 + 5. Don't forget the dot at the end (every statement ends with it)

You didn't write a constraint which uses your newly defined x. As a result of this, FMS thinks you can't be interested in this as it tries to prune as much things away as possible. If you don't want to write a constraint about x, we can use the library function relevant to cheat our way out of this. Now we can write down a working example:

Calculator
x := 4+5.
relevant x.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

The standard operations +/*- are available. Take care that the division operator is integer division, so it truncates. Also the abs function is available which takes the absolute value of a number.

Multiple symbols

It is possible to define multiple symbols and use one to define another. The order of your statements is irrelevant. Now we can define y to be the double of x.

Calculator
x := 4+5.
y := 2*x.
relevant x.
relevant y.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Symbols with local scopes

Sometimes it will be useful to introduce a symbol locally, for example when you want to reuse the result of a complex expression multiple times. This can be done with the let-construct. You could for instance use a let-construct to simplify the expression (3+4)*2+(3+4) to let y:=3+4 in y*2+y. This helps the readability of your expressions. You can also introduce multiple new symbols in a let-construct if you separate them with a semicolon. The order in which these symbols are introduced again does not matter.

Calculator
a := (3+4)+(3+4)*2.
b := let y := 3+4 in y+(y*2).
c := let y := 3+4 ; z := y*2 in y+z.
relevant a.
relevant b.
relevant c.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

A let-construct can introduce shadowing. When you locally define an identifier which was in scope already. The outer-scoped one is hidden and unreachable in the inner expressions.

Calculator
a := 2.
//x is 6 although the outer a is defined as 2
x := let a := 3 in a + a.
relevant x.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

The other way around

Unlike simple calculators, FMS allows you to solve equations with multiple solutions. For this we use variables that can take a range of possible values, and constraints (equations) over these variables.

Declaring a ranged variable is done through name :: element of setExpression. For now we only introduce two kinds of sets (ranges):

  • Contiguous ranges of integers. A range from a to b can be written down as {a..b}.
  • Enumerations. The enumeration of a few constants like {1,2,8,6}.

Then, you can write down the constraints which should hold. All global variables occurring in a constraint are considered relevant, so we do not have to explicitly state this anymore.

Using constraints, it possible to have multiple results. By default all possible results are printed. If you want to override this you can use the statement nbModels n at the top of your file, where the n represents the number of solutions you are interested in. If you set n to 0 it means that you are interested in all solutions.

Calculator
#nbModels 1.
x :: element of {1..10}.
y :: element of {1..10}.
z :: element of {1..10}.
x + y - z = 12.
x - y = 4.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Note that for constraints we use the equals symbol = instead of the definitional equality :=.

Optimization

When there are multiple solutions it is possible that you're interested in an optimal one according to a certain criterion. For this you can add an optimization statement: $minimize or $maximize with a term which needs to be optimized.

Optimization
x :: element of {1..10}.
y :: element of {1..10}.
$maximize (x-y).
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

In this case multiple solutions will still be printed. But each subsequent solution is guaranteed to be better than the previous one.

More than numbers

Strings

FMS also supports strings between double quotes wherever you write a number. The standard lexicographic order applies when comparing strings.

Strings
set := {"a","b","c"}.
x :: element of set.
y :: element of set.
z :: element of set.
x ~= "a".
y = z.
x =< y.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Booleans

The Boolean values true and false are available through the standard library. You can introduce a Boolean variable as a proposition through p :: proposition. This behaves just like p :: element of {true,false}, but it allows for a more efficient implementation. Constraints over propositions can be written with logical connectives | (or), & (and), ~ (not), => <= (implies), <=> (if and only if).

Booleans
a :: element of {1..3}.
b :: proposition.
c :: proposition.
d :: proposition.
b => a = 1.
~c <=> (d | b).
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
Open Source Your Knowledge: become a Contributor and help others learn. Create New Content