Modeling and Verification @ University of Geneva

This repository contains important information about this course. Do not forget to watch it as it will allow us to send notifications for events, such as new exercises, homework, slides or fixes.

Important Information and Links

• Page on Moodle
• Page on GitHub
• Courses are Thursday 14:00 - 16:00
• Exercises are Thursday 16:00 - 18:00
• Gitter is available for chatting

Environment

This course requires the following mandatory environment. We have taken great care to make it as simple as possible.

• Moodle Check that you are registered in the "Modeling & Verification" classroom; we will not use it afterwards.
• GitHub: a source code hosting platform that we will for the exercises and homework. Create an account, and do not forget to fill your profile with your full name and your University email address. Ask GitHub for a Student Pack to obtain free private repositories.
• MacOS High Sierra or Ubuntu 16.04 LTS 64bits, in a virtual machine, using for instance VirtualBox, or directly with a dual boot.
• Atom: a text editor, that we will use to type the sources.

You also have to:

• Watch the course page to get notifications about the course.

• Create a private repository named modelisation-verification (exactly).

• Clone the course repository

  git clone https://github.com/cui-unige/modelisation-verification.git

• Duplicate the course repository into your private one

  cd modelisation-verification
  git push --mirror https://github.com/yourusername/modelisation-verification.git

• Update the repository information

  atom .git/config

  And replace cui-unige by your GitHub username.

• Set the upstream repository:

  git remote add upstream https://github.com/cui-unige/modelisation-verification.git

• Add as collaborators the users: saucisson (Alban Linard) and mencattini (Romain Mencattini).

• Run the following script to install dependencies:

  curl -s https://raw.githubusercontent.com/cui-unige/modelisation-verification/master/bin/install | bash /dev/stdin

The environment you installed contains:

• Git: the tool for source code management;
• Lua: the programming language that we will use;
• Luarocks: a package manager for Lua;
• Atom: the editor we will use. On the first launch, Atom asks to install some missing modules. Do not forget to accept, or your environment will be broken.

Make sure that your repository is up-to-date by running frequently:

  git fetch upstream
  git merge upstream/master

Rules

• You must do your homework in your private fork of the course repository.
• You must fill your full name in your GitHub profile.
• If for any reason you have trouble with the deadline, contact your teacher as soon as possible.
• We must have access to your source code, that must be private.
• Your source code (and tests) must pass all checks of luacheck without warnings or errors.
• Your tests must cover at least 80% of the source code, excluding test files.

Homework

• All homeworks are located in the homework/ directory.
• For warnings about your code, we use LuaCheck. It is already installed in your environment, and can be run using: luacheck src/.
• For testing, we use Busted. It is already installed in your environment, and can run all the tests within *_spec.lua files using: busted src/.
• For code coverage, we use LuaCov. It is already installed in your environment, and can be run using: luacov.

Homework #1

The source files are located within: homework/petrinets/. You have to write code where TODO are located. Do not touch the existing code or tests, but you can add your own tests in addition in a new _spec file.

The deadline is 11 october 2017 at 23:59. We will clone all your repositories using a script, so make sure that @saucisson and @mencattini have read access.

Please install dependencies by running:

luarocks install rockspec/fun-scm-1.rockspec

Evaluation will be:

• have you done anything at the deadline? (yes: 1 point, no: 0 point)
  • [ ] Done anything
• do you have understood and implemented all the required notions? (all: 3 points, none: 0 point)
  • [ ] Reachability graph
  • [ ] Coverability graph
• do you have understood and implemented corners cases of all the required notions? (all: +2 points, none: 0 point)
  • [ ] Reachability graph
  • [ ] Coverability graph
• do you have correctly written and tested your code? (no: -0.5 point for each)
  • [ ] Coding standards
  • [ ] Tests
  • [ ] Code coverage

Homework #2

The source files are located within: homework/adts/. You have to write code where TODO are located. Do not touch the existing code or tests, but you can add your own tests in addition in a new _spec file.

The deadline is 11 october 2017 at 23:59. We will clone all your repositories using a script, so make sure that @saucisson and @mencattini have read access.

Please install dependencies by running:

luarocks install rockspec/fun-scm-1.rockspec
luarocks install rockspec/hashids-scm-1.rockspec

Evaluation will be:

• have you done anything at the deadline? (yes: 1 point, no: 0 point)
  • [ ] Done anything
• do you have understood and implemented all the required notions? (all: 3 points, none: 0 point)
  • [ ] Term Equivalence
  • [ ] Substitution of Variables
  • [ ] Boolean and Natural ADTs
• do you have understood and implemented corners cases of all the required notions? (all: +2 points, none: 0 point)
  • [ ] Term Equivalence
  • [ ] Substitution of Variables
  • [ ] Boolean and Natural ADTs
• do you have correctly written and tested your code? (no: -0.5 point for each)
  • [ ] Coding standards
  • [ ] Tests
  • [ ] Code coverage

Homework #3

The source files are located within: homework/proofs/. You have to write code where TODO are located. Do not touch the existing code or tests, but you can add your own tests in addition in a new _spec file.

The deadline is 15 november 2017 at 23:59. We will clone all your repositories using a script, so make sure that @saucisson and @mencattini have read access.

Please install dependencies by running:

luarocks install rockspec/fun-scm-1.rockspec
luarocks install rockspec/hashids-scm-1.rockspec

Evaluation will be:

• have you done anything at the deadline? (yes: 1 point, no: 0 point)
  • [ ] Done anything
• do you have understood and implemented all the required notions? (all: 4 points, none: 0 point)
  • [ ] Substitutivity
  • [ ] Substitution
  • [ ] Cut
  • [ ] Proof that x+y = y+x
• do you have understood and implemented corners cases of all the required (all: 1 point, none: 0 point)
  • [ ] Substitutivity
  • [ ] Substitution
  • [ ] Cut
• do you have correctly written and tested your code? (no: -0.5 point for each)
  • [ ] Coding standards
  • [ ] Tests
  • [ ] Code coverage

Homework #4

The source files are located within: homework/rewriting/. You have to write code where TODO are located. Do not touch the existing code or tests, but you can add your own tests in addition in a new _spec file.

The deadline is 29 november 2017 at 23:59. We will clone all your repositories using a script, so make sure that @saucisson and @mencattini have read access.

Please install dependencies by running:

luarocks install rockspec/fun-scm-1.rockspec
luarocks install rockspec/hashids-scm-1.rockspec

Evaluation follows the questions:

• have you done anything at the deadline? (yes: 1 point, no: 0 point)
  • [ ] Done anything
• do you have understood and implemented all the required notions? (all: 4 points, none: 0 point)
  • [ ] Rewrite rules in specs
  • [ ] Strategies
• do you have defined an adt that really tests the strategies? (yes: 2 point)
• do you have correctly written and tested your code? (no: -0.5 point for each)
  • [ ] Coding standards
  • [ ] Tests
  • [ ] Code coverage

Homework #5

The source files are located within: homework/ctl/. You have to write code where TODO are located. Do not touch the existing code or tests, but you can add your own tests in addition in a new _spec file.

The deadline is 13 december 2017 at 23:59. We will clone all your repositories using a script, so make sure that @saucisson and @mencattini have read access.

Please install dependencies by running:

luarocks install rockspec/fun-scm-1.rockspec

Evaluation follows the questions:

• have you done anything at the deadline? (yes: 1 point, no: 0 point)
  • [ ] Done anything
• do you have understood and implemented all the required notions? (all: 5 points, none: 0 point)
  • [ ] Rewrite rules to reduce CTL formulas
  • [ ] Computation of CTL formulas
• do you have correctly written and tested your code? (no: -0.5 point for each)
  • [ ] Coding standards
  • [ ] Tests
  • [ ] Code coverage

Homework #6

The source files are located within: homework/dd/. You have to write code where TODO are located. Do not touch the existing code or tests, but you can add your own tests in addition in a new _spec file.

The deadline is 10 january 2018 at 23:59. We will clone all your repositories using a script, so make sure that @saucisson and @mencattini have read access.

Please install dependencies by running:

luarocks install rockspec/fun-scm-1.rockspec

Evaluation follows the questions:

• have you done anything at the deadline? (yes: 1 point, no: 0 point)
  • [ ] Done anything
• do you have understood and implemented all the required notions? (all: 5 points, none: 0 point)
  • [ ] Binary operators on decision diagrams
  • [ ] Filter and map operations
  • [ ] Operation for transitions of the Petri net
• do you have correctly written and tested your code? (no: -0.5 point for each)
  • [ ] Coding standards
  • [ ] Tests
  • [ ] Code coverage