# -*- encoding: iso-8859-1 -*-
# Copyright (c) 2005 Lauri Karttunen
# YaleShooting.txt
#
# This program is free software; you can redistribute it and/or modify
# it under the terms of GNU General Public License as published by
# the Free Software Foundation; either version 2 of the License, or
# (at your option) any later version.
# This program is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
# GNU General Public License for more details.


define Proposition    load | loaded | shoot | alive;
define Valuation      [%+ | %- | F] Proposition ;
define Frame          %[ (Valuation [%, Valuation]*) %];

define Loaded         Frame & $[%+ loaded] & ~$[%- loaded];
define Load           Frame & $[%+ load]   & ~$[%- load];
define Shoot          Frame & $[%+ shoot]  & ~$[%- shoot];
define Alive          Frame & $[%+ alive]  & ~$[%- alive];
define FLoaded        Frame & $[F  loaded];
define FAlive         Frame & $[F  alive];

define InertLoaded    [Loaded & ~FLoaded => _ Loaded | .#.]
                                   &
                      [Loaded => .#. | Loaded | FLoaded _ ];

define InertAlive     [Alive & ~FAlive => _ Alive | .#.]
                                   &
                      [Alive => .#. | Alive | FAlive _ ];

define LoadFLoaded    ~[Load & ~FLoaded];

define ShootFAlive    ~[Shoot & ~FAlive];
define ShootFLoaded   ~[Shoot & ~FLoaded];

echo define YaleShooting   [Alive & ~Loaded]
echo                            Load
echo                           Frame*
echo                           Shoot
echo                           Frame ;
echo

define YaleShooting   [Alive & ~Loaded]
                            Load
                           Frame*
                           Shoot
                           Frame ;

echo Constraining YaleShooting with [ InertLoaded & InertAlive &
echo                                  LoadFLoaded & ShootFAlive & ShootFLoaded];

regex YaleShooting & InertLoaded & InertAlive & LoadFLoaded & ShootFAlive ;

echo Testing...
echo

echo Test 1
echo Succeeds. The target was killed: '-alive' in the last frame.
echo [+alive,-loaded][+load,Floaded,+alive][+loaded,+alive][+loaded,+shoot,Floaded,Falive,+alive][-alive]
up [+alive,-loaded][+load,Floaded,+alive][+loaded,+alive][+loaded,+shoot,Floaded,Falive,+alive][-alive]
echo

echo Test 2
echo Succeeds. The shot missed: '+alive' in the last frame.
echo [+alive,-loaded][+load,Floaded,+alive][+loaded,+alive][+loaded,+shoot,Floaded,Falive,+alive][+alive]
up [+alive,-loaded][+load,Floaded,+alive][+loaded,+alive][+loaded,+shoot,Floaded,Falive,+alive][+alive]
echo


echo Test 3
echo Succeeds. We don't know if the target survived.
echo [+alive,-loaded][+load,Floaded,+alive][+loaded,+alive][+loaded,+shoot,Floaded,Falive,+alive][]
up [+alive,-loaded][+load,Floaded,+alive][+loaded,+alive][+loaded,+shoot,Floaded,Falive,+alive][]
echo

echo Test 4 
echo Fails because '+alive' is missing in Frame 4.
echo [+alive,-loaded][+load,Floaded,+alive][+loaded,+alive][+loaded,+shoot,Floaded,Falive][]
up [+alive,-loaded][+load,Floaded,+alive][+loaded,+alive][+loaded,+shoot,Floaded,Falive][]
echo

echo Test 5
echo Fails because '+loaded' is missing in Frame 3.
echo [+alive,-loaded][+load,Floaded,+alive][+alive][+loaded,+shoot,Floaded,Falive,+alive][]
up [+alive,-loaded][+load,Floaded,+alive][+alive][+loaded,+shoot,Floaded,Falive,+alive][]
echo

echo Test 6
echo Fails because 'Floaded' is missing in Frame 4.
echo [+alive,-loaded][+load,Floaded,+alive][+loaded,+alive][+loaded,+shoot,Falive,+alive][]
up [+alive,-loaded][+load,Floaded,+alive][+loaded,+alive][+loaded,+shoot,Falive,+alive][]
echo