LOGIC FOR
SYSTEMS

Software

Below are software that we will use in the course. Feel free to reach out to TAs if you experience any difficulties in software installation.

Alloy

Alloy should be pre-installed on department machines. If you wish to install it on your own computer, please download and install Alloy 4.2 (Experimental Versions). On Windows, you'll need to install Java x86 to run Alloy. If you have Java x64, you will not be able to use some functionalities, so please install Java x86 and make sure that Alloy is run using the right Java.

In the configuration, please change the setting for Forbid overflows from off (which is the default) to on. On OS X, go to the Options menu and select the last entry. Nothing will appear to happen, but when you look at the menu again, the setting will be on.

Spin

Spin should be pre-installed on department machines. If you wish to install it own your own computer, you can download Spin via the Spin Website.

Rosette

Rosette is provided on department machines, but it needs extra steps to set it up.

  1. Open DrRacket
  2. Go to File > Install Package...
  3. Click "Browse...", followed by "Directory." Navigate the file picker to /course/cs1950y/src/rosette and click "Choose"
  4. Click "Install"
  5. The console will show installation process. There might be an error about error moving documentation: open-output-file: cannot open output file. This is fine and should not affect the installation process, however.
  6. After the installation is complete ("Close Output" button is available), close the window and try entering (require rosette) in the interactive window (REPL). There should be no error.

If you wish to install Rosette on your own computer, you will need to download and install Racket first. After that, follow the instructions provided above, except that in step 3, instead of clicking "Browse...", just type "rosette" in the textbox.