The properties presented in the thesis are verified by executing the
following commands:



Verifying deontic rules 1, 2, 4, and 3, respectively, of Chapter 3:
===================================================================

| ?- verify(travel,travel,_).
where,
initial_state :: a(customer(t), c) ///
		 a(travel_agent([a1],hd,cd),t) ///
		 a(credit_card, cd) ///
		 a(credit_card2,cd) ///
		 a(airline,a1) ///
		 a(airline_booking,_) ///
		 a(hotel_booking,_).

Results are printed in the file 'results_3_dpl.txt' 
(only rule 3 fails).



Verifying Properties 3.2 and 3.1, respectively:
===============================================

| ?- verify(travel,_,travel).
where,
initial_state :: a(customer(t), c) ///
		 a(travel_agent([a1],hd,cd),t) ///
		 a(credit_card, cd) ///
		 a(credit_card2,cd) ///
		 a(airline,a1) ///
		 a(airline_booking,_) ///
		 a(hotel_booking,_).

Results are printed in the file 'results_3_mu.txt'
(only property 3.1 fails).



Verifying Properties 4.3, 4.4, 4.5, and 4.1, respectively:
==========================================================

| ?- verify(vickrey,vickrey,vickrey).
where,
initial_state :: a(auctioneer(cd,5,[b,c],[b,c]),a) ///
		 a(bidder,b) ///
		 a(bidder,c).

Results are printed in the file 'results_4.3_4.4_4.5_4.1.txt'
(only property 4.1 fails).



Verifying Properties 4.2:
=========================

| ?- verify(vickrey,vickrey2,vickrey).
where,
initial_state :: initial_state :: a(auctioneer(cd,5,[b,c],[b,c]),a) ///
		 a(bidder,b) ///
		 a(bidder,c).

NOTE: the fact 'known(a(bidder,_), valuation(_,_))' should replace the
      two facts 'known(a(bidder,b), valuation(_,10))' and
      'known(a(bidder,c), valuation(_,15))'.

Results are printed in the file 'results_4.2.txt'
(nothing fails).



Verifying Properties 5.1, 5.2, and 5.3, respectively:
=====================================================

| ?- verify(request_perform_actions,request_perform_actions_online,request_perform_actions_online).
where, 
the 'realise_goal' constraint is assumed true, and
initial_state :: a(performer,civilian1) /// a(performer,civilian2) ///
	  	 a(requester([(civilian1,transport(neighburs(house23),node1,node2)),(civilian2,move(n3))],_),police) ///
	  	 a(simulator,s).

NOTE: if 'my_time_limit' (which is currently specified within the interaction model) 
      is less than 10, then property 5.2 should fail. 

Results are printed in the file 'results_5.1_5.2_5.3.txt'.



Verifying Property 5.4:
=======================

| ?- verify(info_sharing,info_sharing_online,info_sharing_online).
where, 
initial_state :: a(inquirer(path,R),i) ///
		 a(finder,f1) /// a(finder,f2) /// 
		 a(responder,r1) /// a(responder,r2).

Results are printed in the file 'results_5.4.txt'
(property 5.4 fails).



Verifying Property 5.5 (5.6, 5.7, 5.8, and 5.9 included):
=========================================================

| ?- verify(request_perform_actions,_,request_perform_actions_offline).
where, 
the 'realise_goal' constraint is no longer assumed true, and
initial_state :: a(performer,civilian1) /// a(performer,civilian2) ///
	  	 a(requester([(civilian1,transport(neighburs(house23),node1,node2)),(civilian2,move(n3))],_),police) ///
	  	 a(simulator,s).

This automatically verifies Properties 5.6 and 5.7, respectively, by running:
| ?- verify(route_service,_,realise_goal_route_service).
where, 
initial_state :: a(route_finder(_,_,_,_,_),rf) /// a(route_service, rs).

It also verifies Properties 5.8 and 5.9, respectively, by running:
| ?- verify(info_sharing,_,realise_goal_info_sharing).
where, 
initial_state :: a(inquirer(path,R),i) ///
		 a(finder,f1) /// a(finder,f2) /// 
		 a(responder,r1) /// a(responder,r2).

Results are printed in the file 'results_5.5_5.6_5.7_5.8_5.9.txt'
(only property 5.9 fails).