#!/bin/tcsh
#
# Each line in this file runs af spec validation example.  The order of the
# examples follows the discussion in the 308 lecture notes, in ./308-l7-8.pdf.
#

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

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

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

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

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

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

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

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

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

# Test FindUser with aux functions.
fmsl 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 
