#!/bin/tcsh
#

# The optional $1 is the executable path.  It's sent in from a calling script
# during regression testing.  If this script is called stand-alone from a
# shell, with an empty $1, then the executable is set to "specl", which is
# assumed to be on the path in the invoking she shell.
#
#
# Each line in this script runs a spec validation example.  The order of the
# examples follows the discussion in the 308 lecture notes, in ./308-l7-8.pdf.
#

# If called with empty $1, set the executable to "specl".
if ($1 == "") then
    set specl = "specl"
else
    set specl = $1
endif

# Test the comment-only version of the AddUser spec.
$specl adduser-basic-tests.fmsl adduser-basic.fmsl userdb-objs.fmsl
echo ""

# Test the basic-logic version of the AddUser postcondition.
$specl adduser-basic-formal-tests.fmsl adduser-basic-formal.fmsl userdb-objs.fmsl
echo ""

# Challenge the strength of the basic logic with tests that fail.
$specl adduser-basic-formal-strength-challenge.fmsl adduser-basic-formal.fmsl userdb-objs.fmsl
echo ""

# Test the strengthened AddUser postcondition logic, with successful tests.
$specl adduser-strengthened-tests.fmsl adduser-strengthened.fmsl userdb-objs.fmsl
echo ""

# Run the same tests on the simplified version of postcondition logic.
$specl adduser-strengthened-tests.fmsl adduser-strengthened-simplified.fmsl userdb-objs.fmsl
echo ""

# Run a different style of tests on the constructive postcond logic.
$specl adduser-constructive-tests.fmsl adduser-constructive.fmsl userdb-objs.fmsl
echo ""

# Run the different-style tests on the analytic postcond logic.
$specl adduser-constructive-tests.fmsl adduser-strengthened-simplified.fmsl userdb-objs.fmsl
echo ""

# Test the comment-only version of FindUser.
$specl finduser-basic-tests.fmsl finduser-basic.fmsl userdb-objs.fmsl
echo ""

# Run some validations on the refined verions of Find, Change, and Delete.
$specl find-change-delete-tests.fmsl find-change-delete-basic-formal.fmsl userdb-objs.fmsl
echo ""

# Test FindUser with aux functions.
$specl finduser-with-aux-funcs-tests.fmsl finduser-with-aux-funcs.fmsl userdb-objs.fmsl
echo ""

# Test AddUser flawed precondition.
#fmsl adduser-input-value-checking-tests.fmsl adduser-input-value-checking-weak.fmsl userdb-objs.fmsl

# Test AddUser flawed precondition, case 1.
#fmsl adduser-input-value-checking-tests.fmsl adduser-input-value-checking-weak1.fmsl userdb-objs.fmsl

# Test AddUser flawed precondition, case 2.
#fmsl adduser-input-value-checking-tests.fmsl adduser-input-value-checking-weak2.fmsl userdb-objs.fmsl

# Test AddUser flawed precondition, case 3.
#fmsl adduser-input-value-checking-tests.fmsl adduser-input-value-checking-weak3.fmsl userdb-objs.fmsl

# Test AddUser with fixed precondition.
#fmsl adduser-input-value-checking-tests.fmsl adduser-input-value-checking.fmsl userdb-objs.fmsl

# Test FindUser seg faulting version; now fixed.
# fmsl finduser-seg-faults.fmsl userdb-objs.fmsl 
