Specification and Verification Tools Seminar Homework 4 $Date: 2008/10/26 23:13:11 $ For October 8, 2008. Download and install Discrete Event Calculus Reasoner from http://decreasoner.sourceforge.net/ . Then follow the instructions in the README file included with the release. However, note that relsat from is availble from http://www.bayardo.org/resources.html or http://www.bayardo.org/bin/relsat_2.02.tar . On cygwin I unzipped to software/relsat-dist and then to compile relsat I used cd software/relsat-dist make -f Makefile.linux mv relsat.exe ../../solvers/ instead of using the script (makerelsat_cygwin.sh) mentioned in the README file. You also have to get PLY, it seems that you should get version 1.6 instead of the latest version. Then the makeply.sh script will work. Read the Discrete Event Calculus Reasoner User's Manual from http://decreasoner.sourceforge.net/csr/decreasoner.pdf While reading, play with Discrete Event Calculus Reasoner to test out questions you have. (You can also bring questions to the seminar.) PROBLEM Make a representation of program execution of multiple machines. Assume that each program has one input file and one output file. -There are host machines, files and programs. -There are files on host machines. The name identifies a file. You can have copies of the same file on multiple machines. Files can be created, deleted, or FTPd from one machine to another (which creates it on the target machine). Files can be renamed or copied to a different file. -Executing a program creates its output file. A program can not be executed if its input file does not exist on the same machine. Examples to run: -see the changes triggered by a set of events and actions. -what kind of actions need to be run to achieve a certain state of the world (eg. files FINALOUTPUT exists on machine HOST_USER).