Description
CSC410 Assignment 1
Problem 1 (20 points) Below, you can see a function that sorts an array. This a simpler sorting routine called insertion sort. The goal is to verify partial correctness of this implementation. Naturally, we expect a sorting routine to return a sorted array. In case you are wondering, you do not have to verify that the resulting array and the original one contain the same set of elements. method insertSort(a : array) { var i := 1; while (i < a.Length) { var j := i; var value := a[i]; a[i] := a[i-1]; while (j > 0 && a[j-1] > value) { a[j] := a[j-1]; j := j – 1; } a[j] := value; i := i + 1; } } (a) What are the appropriate precondition and postcondition for this function? Naturally, we want sortedness as part of the postcondition! (b) What are the (inductive) loop invariants? Note that there are two while loops in this example. You will submit a Dafny file containing the code with your pre/post-conditions and loop invariants that successfully runs through Dafny. Keep in mind that your assignment will be graded automatically. If it does not go through Dafny, you will get no marks. Do not forget: no assignment will be accepted from a group of less than 3 students. Find your groupmates today! You can use pizza’s feature for this or just talk to your classmates in class. Problem 2 (50 points) The following “elegant” sort algorithm gets its name from the Three Stooges slapstick routine in which each stooge hits the other two. Hint: this is a bit tricky. Try to elaborate on ”what” we know about the contents of each 1/3rd array after each recursive call, with respect to the content of the other two 1/3rd arrays. method stoogeSort(a : array, left : int, right : int) { 1 if (a[left] > a[right]) { // swap a[left] and a[right] var tmp := a[left]; a[left] := a[right]; a[right] := tmp; } if (left + 1 >= right) return; k := (right – left + 1) div 3; stoogeSort(a,left, right – k); // First two-thirds stoogeSort(a,left + k, right); // Last two-thirds stoogeSort(a,left, right – k); // First two-thirds again } • What are the appropriate precondition and postcondition for this function? Naturally, we want sortedness as part of the postcondition! You will submit a text file containing the code with your pre/post-conditions that successfully runs through Dafny. Naturally, this file will include functions, lemmas, and all the extra goodies you require to prove that the function correctly sorts. Like the previous example, the aspect of the proof that the sorted array is a permutation of the original array elements may be skipped as the post condition. Note: this is your hardest problem. The reason is that unlike Problem 3, we have not already provided you with the ”intuitive” reason why the code above correctly sorts, and only left the formalization for you. You need to first conceptually find that reason, and then formalize it. Problem 3 (50 points) This solution is based on a known puzzle, “catch a spy”. The purpose is for us to practice using a theorem prover, like Dafny, to do a formal proof that is not related to program. The puzzle and its solution are effectively provided to you (and you can consult resources online for this). We are not asking you to find a solution for the puzzle. We are asking you to use Dafny to prove formally that the provided solution for the puzzle is indeed correct. The spy exists on a one-dimensional line. His location is described by the expression a+t∗b, where a, b ∈ N are unknown constants and t ∈ N is the number of seconds since he pirated your work. Unfortunately, he has also stolen U of T’s cloak of invisibility, so our only means to find him is to physically query a single location every second. That is, at every second, we may ask “is the spy at location n” and get back a “yes” or “no” answer. We can catch the spy as follows. The set N×N of pairs of natural numbers is countable, so there exists a function unpair : N → N × N that covers all pairs of natural numbers. Our strategy is to check the location x + t × y at time t, where (x, y) = unpair(i). Since there exists some t0 such that (a, b) = unpair(t0), then at time t0 we will check the location a + t0 ∗ b and therefore catch the spy. Complete the implementation of unpair according to our strategy above, and prove that the while loop terminates (i.e. that we eventually catch the spy). function method unpair ( i : nat ): ( nat , nat ) { // TODO } function method pick ( i : nat ): nat { var (x , y ) := unpair ( i ); x + i * y } method catchTheSpy ( a : nat , b : nat ) { 2 var i := 0; while a + i * b != pick ( i ) { i := i + 1; } } You may use any valid implementation of unpair : N → N × N, but the Cantor pairing function is suggested. The Cantor pairing function essentially lists all pairs who’s sums are 0, then all pairs who’s sums are 1, and so on. unp ai r ( 0 ) = ( 0 , 0 ) unp ai r ( 1 ) = ( 0 , 1 ) unp ai r ( 2 ) = ( 1 , 0 ) unp ai r ( 3 ) = ( 0 , 2 ) unp ai r ( 4 ) = ( 1 , 1 ) unp ai r ( 5 ) = ( 2 , 0 ) . . . On 2017/09/25: minor typo fixed above. The return type of unpair was mistakenly left as a single “nat” before. But, its use in pick already indicated that it is meant to return a pair of elements. 3
CSC410 Assignment 2
For each problem, you will write a wrapper code, in your language of choice, such as Python, Perl, C, etc
that reads an input text file (as specified for each problem) and generates the output file, and a formula file
that contains the exact goal that you submit to z3 for checking (in the same directory where we execute your
code). The formula file will serve as a side-sanity-check for us to make sure you are doing things properly.
Your wrapper processes the input file, constructs the formula, discharges the satisfiability goal to z3, and
processes the output provided by z3 to construct the (well-formatted) output for each problem (as specified
in each case).
We will expect a command-line executable (on CDF/CSLab machines) file named:
• hidato (for problem 1)
• grouping (for problem 2)
We will test your answer on CDF/CSLab machines by placing all your files in a single directory and invoking
(for example)
hidato input-file
from the command-line.
Summary of files you provide and the output files your tool should generate:
• Hidato
– An executable called hidato. This should be executable on CDF (without a need for paths,
…). We will basically type hidato sample-input-file-name, and your program should run and
produce the desired outputs.
– All source files for this executable (for inspection purposes) as a zipped directory hidato.zip
– As a result of running your executable on a text input file (as specified), we will expect two output
files: hidato-output.txt which includes the correct answer (as specified), and hidato-formula.smt2
which includes the formula you submit to z3 to solve the puzzle.
• Grouping
– Executables called groupinga and groupingb. This should be executable on CDF (without a need
for paths, …). We will basically type groupinga sample-input-file-name, and your program
should run and produce the desired outputs.
– All source files for the executables (for inspection purposes) as a zipped directory grouping.zip
– As a result of running your executable on a text input file (as specified), we will expect two output
files: groupinga-output.txt which includes the correct answer (as specified), and groupinga-formula.smt2
which includes the formula you submit to z3 to solve the puzzle (repeat for the groupingb instance).
Evaluation method: We will test each problem with a few different inputs (5–10). For each correct
output, you will get an equal fraction of the problem points. In other words, if your code returns the correct
output on all tests, you will get a full-mark, and for every wrong answer you will loose (proportionally) some
points. Beyond this, there are no partial marks for any partial efforts.
1
Problem 1
[30 points] Hidato is a famous puzzle game. You may have already played this game on your phone. If not,
the time has finally come for you to know about it:
https://en.wikipedia.org/wiki/Hidato
Use your theory of choice to formulate a Hidato puzzle solver: “Given a partially completed grid, is it possible
to complete the grid obeying the rules of Hidato?” If the answer is no, then a simple “NO SOLUTION” in
the output is sufficient. If the answer is yes, then you need to provide the completed grid as an output.
Input format. The partially completed grid will be provided to you with “-” standing for each blank cell
(to be filled by a number) and “*” standing for blocked cells (not to be filled by any numbers) each two
symbols separated by a single space. Each line of the puzzle is written in a separate line of the input file.
For example, the input file:
* * 7 6 – * *
* * 5 – – * *
31 – – 4 – – 18
– 33 2 12 15 19 –
29 28 1 14 – – –
* * – 24 22 * *
* * 25 – – * *
represents the game (to be played):
* * 7 6 * *
* * 5 * *
31 4 18
33 2 12 15 19
29 28 1 14
* * 24 22 * *
* * 25 * *
is an input file for which your output should be:
* * 7 6 9 * *
* * 5 8 10 * *
31 32 3 4 11 16 18
30 33 2 12 15 19 17
29 28 1 14 13 21 20
* * 27 24 22 * *
* * 25 26 23 * *
that corresponds to the solved puzzle:
* * 7 6 9 * *
* * 5 8 10 * *
31 32 3 4 11 16 18
29 33 2 12 15 19 17
29 28 1 14 13 21 20
* * 27 24 22 * *
* * 25 26 23 * *
Do not forget: your wrapper code (in your programming language of choice) is meant to only read the
text grid, and output a formula F (in the theory of your choice) where a satisfiable assignment to F is a
solution to puzzle. You are not allowed to do any other ”solving” in your programming language. All puzzle
solving needs to be deferred to z3. If you do any solving in your wrapper code (even if it is a little bit), you
will get a zero for this problem.
2
Problem 2
Consider the situation that the students in a class want to team up in groups of (exactly) 2 students for a
course project. The instructor asks each student to submit a list of partners that they are willing to work
with. These lists are not prioritized, in the sense that it is understood that a student would be equally
happy to work with anyone on her/his list. After all lists are in, the instructor is faced with the challenge of
making as many groups of 2 as possible respecting students’ wishes. The goal of this problem is to write a
small program to help “her”.
Write a wrapper program that takes the lists of student preferences as an input, and prints in the output
the groups (of two students) formed, with the understanding that as many students as possible have been
grouped together. You will solve this problem in two ways:
(a) (30 points) You can only use the theory of propositional logic (boolean variables only) for the purposes
of this subproblem. Solutions that use richer theories such as linear arithmetic or equality logic will
get no credit.
(b) (30 points) You can only use a richer theory of your choice. Note that the theory does not have to be
theoretically strictly more expressive; therefore, equality logic with uninterpreted functions (reducible
to propositional logic) is acceptable for this.
Keep in mind that the encoding should be genuinely different in this case compared to (a), in the
sense that you will not add superficial bells and whistles to (a) to get (b). Since this theory subsumes
propositional logic, it is certainly possible to do the superficial thing. But, that solution will get zero
credit. So, in this case think integer variables instead of booleans, and genuine non-boolean constraints.
The purpose of the exercise is for you to contrast two different encodings of the same problem against
each other, in terms of (i) the ease of encoding, (ii) the size of encoding, and (iii) the performance of
the solver at the end. You will submit a pdf file (grouping.pdf) containing a short report to let us
know about your conclusions regarding (i–iii). Make clear claims, and back them up by solid evidence.
But, don’t be verbose. There are 10 points dedicated to this report, which will bring the total for the
homework to 100 points.
Do not forget, in each case, like problem 1, you cannot do any solving in the wrapper code. It should
be solely for the purpose of generating and dumping a formula to z3, which will then produce the optimal
solution (including the optimization part) for you. This is in the spirit of the job shop problem you saw
in the tutorial. For (a), you will be using the assert-soft command (not covered in the tutorial), but
explained in the online Z3 tutorial.
Input format. For simplicity, we identify students with integer identifiers 1 . . . n (where n is the number
of students in the class). The input will have one line per student in which a (space separated) list of id’s
appear indicating the student’s choice. For example, in a class with 5 students, the following input:
2 3 4
1 3 5
2 1
1
2
illustrates the partner choices of student “1” as {2, 3, 4}, and the partner choices of student “5” as just a
single student “2”. The correct (maximal) output for this case then is:
2 groups formed:
1,4
2,5
or
2 groups formed:
1,3
2,5
3
It is understood that there is only one answer for the optimal number of groups that can be formed, but
the arrangement of students into groups that would produce that optimal number may not be unique.
The number should be correct, but any valid arrangement is fine. You do not need to produce all valid
arrangements for the optimal answer.
Note: This is a computationally hard problem. It could be expected, depending on the quality of your
encoding, that your code will not scale to large instances. That said, your code (even if correct) should
not be so bad in quality that it cannot solve small instances like the example given above. So, like any
other code, reasonable performance is part of the specification together with correctness. If a group’s code
substantially outperforms everyone else’s (in solving large instances), then I will consider a bonus prize (in
the form of extra marks) for that group.
Repeat Warning
The purpose of these exercises is to solve these problems using a reduction to a satisfiability problem. If
you write a program that solves the same problem algorithmically, you will not get any credit for it. The
reason that we ask for the formula file is to verify that you are indeed doing the reduction. The wrapper
program should only process input, generate formulas, and clean up outputs. All the problem solving should
be deferred (by way of a correct encoding) to Z3. You have now been warned numerous times in a short
document about this single issue. There will be zero leniency regarding mistakes of this type.
Extra
If you are a genuinely interested student, I encourage you to try to separately program direct solutions
for either of these problems and compare your solution to the wrapper+solver combination. It would be
interesting to see if yours is better or worse, and how long each solution takes. This is just a suggestion for
you and has no bearing on the homework or its mark.
4
CSC410 Assignment 3
Problem 1
Upwards Exposed Uses. Upwards exposed uses serves a similar purpose to reaching definitions analysis.
Instead of finding which definitions reach each point, we find which uses of a variable have not yet been
matched with one or more definitions. Given a control flow graph hV, Ei the use of the variable x at vertex
v is upwards exposed at a vertex u (i.e., hx, vi ∈ UEU(u)) if
• x is read at v, and
• there exists a path from u to v along which no vertex assigns to x.
(a) (10 points) Formally define the property space for this problem (i.e. a set and its corresponding meet
operator).
(b) (20 points) Define the (statement) transformer functions for this analysis (stick to the simple language
that is used on the slides for all the other example analyses that you have seen).
(c) (10 points) Fully define the analysis by characterizing whether it is forward or backward, what the
initial nodes are, and what value is given to these initial nodes and all the other nodes before the
default iterative work-list algorithm starts.
(d) (60 points) Having done all of the above properly, implement your design in SOOT and get an analyzer
for the upward exposed uses analysis.
Assignment Format and Guidelines on Submission
For this assignment, you will be implementing data flow analyses using SOOT, which was introduced to you
during the last tutorial.
For the problem you are given the base Java code. You will modify the file UpwardExposedUses.java.
You will not edit any other file. You are expected to submit only the file UpwardExposedUses.java.
(Any helper or additional classes you may need to create should be created within this file itself).
You must create your UpwardExposedUses class by extending any of the Data Flow Analysis classes
provided by Soot, and overriding the appropriate functions accordingly. You must not use any library or
package (other than Soot) or code from any such library or package- all code you submit must be your own.
1
Input-Output Format
The input will be in the form of a Java .class file. For the output you should print all the upward exposed
uses to a file called exposed-uses.txt in the same location from where the code is run.
Note that you should not print the upward exposed uses to STDOUT. Any output to STDOUT or
STDERR will be ignored. If the program creates any .jimple/.jimp files in the directory sootOutput, let
them stay there; you should not delete them.
Printing upward exposed uses
You should print, to the file exposed-uses.txt, all upward exposed uses with each upward exposed use
taking exactly 3 lines. If the the use of the variable x at node v is upwards exposed at the exit of node u
(i.e. if hx, vi ∈ UEU(u)) then you would print on the first line the node u, on the second line the node v,
and on the third line the variable x. Make sure you have the order correct. You should make sure that each
node fits within a single line. If any node takes up more than one line, remove all newline characters from
the output of the node.
z = 2
y = 10
x = y*z
For example in the case of the above code, there are just three nodes in the graph- z = 2 y = 10, and x =
y*z, in which case the output to the file exposed-uses.txt should be:
z = 2
x = y*z
z
y = 10
x = y*z
z
y = 10
x = y*z
y
While actually running your code for the above case the names of the nodes, branch labels, and variables
in the control flow graph passed to your analysis class may vary slightly depending on Soot’s pre-processing,
and so the names of the nodes and variables printed to the file may be different; that is okay.
You may print the exposed uses in any order. But you should cover all upward exposed uses for the
exit points of all nodes and you should not repeat the same exposed use twice in the file. You are given a
particular test case and its expected output in the base code.
Evaluation
We will test your answer on CDF/CSLab machines by placing your submitted UpwardExposedUses.java
file in the base code source directory, compiling it, and running it on examples. The code should compile
and run as in the test.sh script. You should make sure your UpwardExposedUses.java file compiles and
runs with the provided base code on CDF/CSLab machines.
The code will be tested on different examples. For each correct output, you will get an equal fraction
of the problem points. In other words, if your code returns the correct output on all tests, you will get a
full mark, and for every wrong answer you will lose (proportionally) some points. Beyond this, there are no
partial marks for any partial efforts.
2
If the code fails to compile, returns a runtime error due to your fault, or fails to print the
results in the correct format to the exposed-uses.txt file you may not get any marks.
Summary of submission files
• A PDF file for parts (a-c). Call it hw3.pdf.
• The file UpwardExposedUses.java as described above for part (d).
3
CSC410 HW 4
Problem 1
A Bit Vector Framework is a special instance of a monotone framework where
• L = (P(D), u) for some finite set D and where P(D) is the powerset of D and u is either set union
(∪) or set intersection (∩), and
• F = {f : P(D) → P(D)| ∃G, K ⊆ D : ∀S ⊆ D, f(S) = (S ∩ K) ∪ G}.
You will hand in a pdf containing the written answer to the following questions:
(a) (15 points) Show that Live Variable Analysis is a bit vector framework (this is mostly trivial).
(b) (25 points) Show that all bit vector frameworks are distributive frameworks.
(c) (10 points) Provide an example of a simple distributive framework that is not a bit vector framework
to prove (by counterexample) that the converse of (b) is not true.
Note that you are not being asked to remember something you have seen for this before, but to make up
a small example that satisfies this condition. The example does not have necessarily have to correspond
to a real widely used analysis. Anything that fits the definition of an analysis over a program will be
acceptable.
This is a variation of exercise 2.9 in the book.
Problem 2
This problem is long, but it is very simple and has a rather short solution. It is long, because I wanted to
simplify it by walking you through the solution steps, and give some examples. The solution to each part is
short and simple. You just need to be careful with part (c).
Simpler data flow analyses can be composed to make a more sophisticated one. Let us try to do this
together to learn how it is done. We pick a (more) sophisticated data flow analysis, called partial redundancy
elimination (PRE) as our target.
Available expressions analysis (see page 39 of your assigned reading) is a simple analysis that captures
the redundancy of an expression along all paths (i.e. complete redundancy). However, in some situations,
an expression may be only partially redundant along, that is redundant along some path, but not redundant
along some other. Consider the diagrams below:
1
g(),pyythe path 2 → 3, only one computation of x ∗ y occurs on the path. However, along the path 1 → 3,
two computations of x ∗y occur. Thus, x ∗y is partially redundant in node 3. This redundancy can be
eliminated by inserting x ∗ y in node 2; this makes its computation in node 3 completely redundant,
which can then be eliminated. This can also be seen as hoisting expression x ∗ y from node 3 into
node 2 (Figure 1.3(b)).
1 x * y 2
3 x * y
(a)
1 x * y 2
3
x * y
(b)
FIGURE 1.3 Partial redundancy elimination.
The expression x ∗ y is redundant on the path from 1 to 3, but not from the path from 2 to 3 (in (a)). The
expression is clearly not available (in the sense of available expressions) at node 3. But, if we insert x ∗ y
into node 2, then it becomes completely redundant in node 3. The precise criterion for PRE is quite subtle;
intuitively, the expression must be partially redundant at a node (say i) and some predecessors of i must
exist in which the expression can be inserted without changing the semantics of the program.
The principle of performing partial redundancy elimination is to introduce new computations of the
expression at points of the program chosen in such a way that the partially redundant computations become
redundant and can hence be deleted. In the example above, the identification of node 2 is the key to deleting
the redundancy at node 3.
To make up a partial redundancy eliminator, we introduce, and then combine a few simple (basic) analyses
through the following steps.
(a) (10) An expression is partially available at a program point ` if it there is at least one control flow path
to location ` along which the expression is computed, and none of its operands have been overwritten
since. Note the contrast against available expressions. With a minor change to the formal definition
of available expressions analysis, you can get a definition for partially available expressions. Make this
precise, by providing the constraints (equations) that formally define partially available expressions.
Note that we are asking you to cut-and-paste the formal definition form available expressions and make
a few simple changes to them to get the new analysis. Do not overthink this. It is trivial.
(b) Anticipability is the dual of availability. An expression is anticipated at a location ` if it computed
along all (future) paths from `, and none of its operands are modified on each path until the first
computation of the expression. This is what is named as very busy expressions analysis in your text
book. There is nothing to do for part (b), other than reminding yourself of this definition to use it in
(c).
(c) (30) Placement Possible Analysis aims to determine predecessors of a statement, which contains partial
redundancies, where a new computation may be introduced. Define a data flow analysis for placement
possible by providing the property space, the transfer functions, and the initialization information. The
idea is that you will use available expressions, very busy expressions, and partially available expressions
in your data flow equations for placement possible analysis.
Note: this is intentionally loosely defined. Making this definition precise is part of the exercise.
(d) (10) To wrap this up, provide two equations defining the two key sets:
– insert `: the set of the expressions that must be added as new computations at location `. The
new computation would be inserted at the exit from the node (i.e. after all the statement(s)
already there in the node).
– delete`: the set of redundant expressions that may now (after the inserts above) be deleted from
the location `.
Note that the two sets above should be computable from the result of analyses in the previous part.
We are not setting up new data flow analyses to compute them in part (d). At this point (specially
after part (c)), all the ingredients should be there for you to compute the insert and delete sets using
simple set operations over the results of the analyses that you have already defined.
For those following things carefully, there should be a question on your mind at this point: are the
answers to this analysis really unique? Well, not exactly. This is a compiler optimization technique that was
introduced to subsume a few other simpler optimizations. The goal with its design was to cover the simpler
cases, and do more but not ”do everything!”. So, your design should have the following properties:
2
• It should do no harm. At the end of the transformation no path of the graph can contain more
computations of an expression than it contained before. This may seem sensible, but has serious
consequences. For example, an expression cannot be inserted in a place where now it will become
known to a path where it was not known before. For example, in the figure below:
x + y
x + y
a b
d c
the redundancy at node c cannot be eliminated because moving the computation to a will introduce
the expression x + y to the path a → d where it was not available before.
• A partial redundancy is being suppressed by possibly introducing new partial dependencies. The
recursive nature of the problem means that a global optimization is best performed during runtime.
You do not have to worry about the new partial dependencies that your inserts are creating, as long
as you are maintaining the property from the previous bullet point.
• Your analysis does not have to always insert the minimal number of computations. Following to the
point above, new inserts may be redundant or partially redundant and can be replaced by fewer inserts
in another round of this algorithm. Do not worry about minimality.
• One can design the analysis to do nothing and still satisfy the two conditions above. So, here are a
couple of examples that your analysis should be able to handle by performing the illustrated transformations. Below, the graph on the left should be transformed to the graph on the right (the red x
indicates that node 4 modifies x):
1
2
3 4
5 6
7
8
9
x + y
x + y
x + y
x + y
x
1
2
3 4
5 6
7
8
9
x + y
x + y
x
Moreover, the expression x + y should be in the placement possible in sets of nodes 1, 2, 3, and 4, and
in the placement possible out sets of nodes 3, 4, 5, 6, 7. Naturally, the resulting graph says that the
insert set of only nodes 3 and 4 shall end up including the expression x + y, and the delete sets of 6,
7, 8, and 9 should include x + y.
Another example is the following generic optimization which is referred to a loop invariant optimization,
which your partial redundancy elimination should subsume. In the classical optimization, computation
of an expression is removed from a (nested) loop while it is both invariant in the loop and can be
anticipated on entry. The diagram below graphically illustrates this transformation from the redundant
version (left) to the optimized version (right):
3
1
2
3
4
5
6
x + y
x + y
1
2
3
4
5
6
x + y
4
CSC410 Assignment 5
Problem 1
(50 points) Four wounded soldiers find themselves behind enemy lines and try to flee to their home land.
The enemy is chasing them and in the middle of the night, they arrive at a bridge that spans a river which is
the border between the two countries at war. The bridge has been damaged and can only carry two soldiers
at a time. Furthermore, several landmines have been placed on the bridge and a torch is needed to sidestep
all the mines. The soldiers only have a single torch and they are not equally injured. The extent of their
wounds have an effect on the time it takes to get across. The time needed for soldiers to pass the bridge are
respectively 5, 10, 20, and 25 minutes respectively.
(a) (20 points) Construct a model of this problem in NuSMV and then reduce the question ?can all soldiers
cross the bridge in 60 minutes or less? to model checking problem by stating the question as an LTL
property.
Make sure that your model will include all possible scenarios for crossings (even pointless ones such as
one soldier takes the torch to the other side and then comes back). Like our homework 2, it is not your
job to partially solve the problem and encode any solution into the model. The model should just rule out
moves that are made impossible by the storyline above. Anything move that can be taken (by the stupidest
possible problem solver) should be part of the model.
Next, we use the model and the power of model checker to solve the problem given different requirements
for the solution. The solution requirements are listed below. For each item, one property (i.e. one LTL
formula), checked through the model is the answer that we require.
(b) (5 points) Can all soldiers eventually cross the bridge? Note that this is a yes/no question.
(c) (5 points) Can you rephrase the first property so that you get the model checker to tell you the
step-by-step scenario under which all soldiers can cross the bridge?
(d) (5 points) Is there a scenario in which only one soldier is left at the enemy side of the bridge? (yes/no
question)
(e) (5 points) Can you rephrase property (c) so that you get the model checker to tell you how to get all
soldiers across the bridge within 60 minutes?
Submission Guidelines. You will use the model checker NuSMV for the purpose of this exercise. It is
installed on the teaching clusters. You will submit a text file called soldiers.smv which will contain the model
and the properties listed (in the same order as the itemized list above).
Problem 2
(10 points) Consider the transition system T S over the set of atomic propositions AP = {a, b, c}:
Exercises 301
fulfilled:
(a) ! a
(b) !!! a
(c) ! b
(d) ! ♦a
(e) ! (b Ua)
(f) ♦(aUb)
Exercise 5.2. Consider the transition system TS over the set of atomic propositions AP =
{ a, b, c }:
s1
{a}
s3
{b, c}
s2
{c}
s5
{a, b, c}
s4
{b}
Decide for each of the LTL formulae ϕi below, whether T S |= ϕi holds. Justify your answers! If
T S “|= ϕi, provide a path π ∈ P aths(T S) such that π “|= ϕi.
ϕ1 = ♦ ! c
ϕ2 = ! ♦c
ϕ3=!¬c→!!c1
Decide for each of the following LTL formulae φi below, whether T S |= φi
. Justify your answers. Informal,
but solid justifications suffice. If T S 6|= φi
, provide a counterexample as your justification.
φ1 = ♦c
φ2 = ♦c
φ3 = ¬c =⇒ c
φ4 = a U (b ∨ c)
φ5 = ( b) U(b ∨ c)
Problem 3
(31 points) Which of the following equivalences are correct? Prove the equivalence or provide a counterexample that illustrates that the formula on the left and the formula on the right are not equivalent. For
proofs, you are allowed to use the equalities that were already presented to you in class. But keep in mind
that they may not solve all items. You need to refer to semantic definition of operators to get some of the
proofs through. Naturally, you can do all the proofs directly using the semantic definitions.
(a) ♦φ ≡ ♦ φ
(b) ♦φ =⇒ ♦ψ ≡ (φ =⇒ ♦ψ)
(c) (♦φ1) ∧ (♦φ2) ≡ ♦(φ1 ∧ φ2)
(d) ♦φ =⇒ ♦ψ ≡ (φ U(ψ ∨ ¬φ))
(e) φ =⇒ ♦ψ ≡ φ U(ψ ∨ ¬φ)
Reminder: for the purposes of proving (or disproving) the equalities, you can either use the direct semantics
of and ♦ or use equalities ♦φ ≡ true U φ and φ ≡ ¬♦¬φ.
Problem 4
(9 points) Let φ and ψ be LTL formulae. Consider the following new operators.
(a) “At next” (φ N ψ): at the next point in time where ψ holds (is true), φ also holds.
(b) “While” (φ W ψ): φ holds at least as long as ψ does.
(c) “Before” (φ B ψ): if ψ holds at some point in the future, φ holds before.
Make the definitions of these informally stated operators precise by providing LTL formulae that formalize
their intuitive meaning.
2
