%%%%%
%%%%% SIGNATURE

A,A1 :: agent(A).
L,L1 :: location(L).

agent(emerson).
agent(thoreau).

location(harvard).
location(walden).

fc(loc(A)).
fc(pleased(A)).
fc(turbulent(A)).
domain(loc(A), L).

ac(A^move).
oblpac(A^writeTo^A1) :-
 A \= A1.

domain(A^move, L).
domain(A^move, ff).

%%%%%
%%%%% SYSTEM

caused loc(A)=L after A^move=L.
nonexecutable A^move=L if loc(A)=L.

caused pleased(A1) after A^writeTo^A1 :-
 A \= A1.
caused -turbulent(A) after A^writeTo^A1 :-
 A \= A1.

%caused -pleased(thoreau) if loc(thoreau)=harvard.

%%

inertial FC :-
 fc(FC).
exogenous A^move.

%%%%%
%%%%% NORMS

local_global.

% if Thoreau is at Walden, nobody else must be there

notpermitted loc(thoreau)=walden if loc(A)=walden :-
 A \= thoreau.

% Emerson ought not go to Harvard unless Thoreau goes too

emerson notpermitted emerson^move=harvard & -(thoreau^move=harvard).

% Thoreau should not to write to Emerson from Walden

thoreau notpermitted thoreau^writeTo^emerson if loc(thoreau)=walden.

%%%%%
%%%%% Policies

% Any epistolary activity, except if it is explicitly denied by pol

top ptop is (pol or (neg pol)).

pol @ {
 % Emerson is not allowed to write to Thoreau while he's at Harvard
 denied(emerson^writeTo^thoreau) if loc(emerson)=harvard
}.

% Emerson must write to Thoreau when he is feeling turbulent

caused obl(emerson^writeTo^thoreau) if turbulent(emerson).

%%%%%
%%%%% Queries

% Are there (globally) red transitions where everyone fulfils
% their obligations?

query(rfulf, 1, [0:trans=red|List]) :-
 findall(-(0:viol(S^Act)), (oblpac(S^Act)), List).

% If Ag fulfils his agent-specific norms, does that mean he violates no
% obligations?

query(fnv(Ag, Act), 1, [-(0:red(Ag)), 0:viol(Ag^Act)]) :-
 agent(Ag),
 oblpac(Ag^Act).

% Show transitions to a red state where no norms are violated

query(rsf, 1, [1:status=red|List]) :-
 findall(-(0:viol(S^Act)), (oblpac(S^Act)), List).