%==============================================================================
% Project:	Microcontroller Programming in Datalog
% Version:	0.4
% Filename:	examples.pl
% Purpose:	Data of the blink0 example and another test case
% Last Change:	29.03.2021
% Language:	Prolog (tested with SWI Prolog)
% Author:	Stefan Brass
% Email:	brass@informatik.uni-halle.de
% WWW:		http://www.informatik.uni-halle.de/~brass/
% Address:	Univ. Halle, Von-Seckendorff-Platz 1, D-06120 Halle, GERMANY
% Copyright:	(c) 2020-2021 by Stefan Brass
%==============================================================================

% For more information, see the main file: ctest.pl


%******************************************************************************
% Data of the Examples:
%******************************************************************************


%==============================================================================
% The Blink Example from the Paper (blink0):
%==============================================================================


%------------------------------------------------------------------------------
% blink0_rule(No, Head, BodyList):
%------------------------------------------------------------------------------

% Variables are encoded v(VarName). VarName should not end in a digit.

blink0_rule(1,
	call_pinMode(0,13,output),
	[]).
blink0_rule(2,
	turn_on(1),
	[]).
blink0_rule(3,
	delayed_turn_off(v('S'), v('From'), 1000),
		[turn_on(v('T')),
		ret_millis(v('T'), v('From')),
		succ(v('T'),v('S'))]).
blink0_rule(4,
	delayed_turn_off(v('S'),v('From'),v('Delay')),
		[delayed_turn_off(v('T'),v('From'),v('Delay')),
		ret_millis(v('T'),v('Now')),
		plus_lt(v('From'), v('Delay'), v('Now')),
		succ(v('T'),v('S'))]).
blink0_rule(5,
	turn_off(v('S')),
		[delayed_turn_off(v('T'),v('From'),v('Delay')),
		ret_millis(v('T'),v('Now')),
		plus_ge(v('From'), v('Delay'), v('Now')),
		succ(v('T'),v('S'))]).
blink0_rule(6,
	delayed_turn_on(v('S'),v('From'),1000),
		[turn_off(v('T')),
		ret_millis(v('T'),v('From')),
		succ(v('T'),v('S'))]).
blink0_rule(7,
	delayed_turn_on(v('S'),v('From'),v('Delay')),
		[delayed_turn_on(v('T'),v('From'),v('Delay')),
		ret_millis(v('T'),v('Now')),
		plus_lt(v('From'), v('Delay'), v('Now')),
		succ(v('T'),v('S'))]).
blink0_rule(8,
	turn_on(v('S')),
		[delayed_turn_on(v('T'),v('From'),v('Delay')),
		ret_millis(v('T'),v('Now')),
		plus_ge(v('From'),v('Delay'),v('Now')),
		succ(v('T'),v('S'))]).
blink0_rule(9,
	call_digitalWrite(v('T'), 13, high),
		[turn_on(v('T'))]).
blink0_rule(10,
	call_digitalWrite(v('T'), 13, low),
		[turn_off(v('T'))]).
blink0_rule(11,
	always(0),
	[]).
blink0_rule(12,
	always(v('S')),
		[always(v('T')),
		succ(v('T'),v('S'))]).
blink0_rule(13,
	call_millis(v('T')),
		[always(v('T'))]).

%------------------------------------------------------------------------------
% blink0_constraint(ID, Lit1, Lit2, Formula):
%------------------------------------------------------------------------------

% Variables are encoded v(VarName). VarName should not end in a digit.

blink0_constraint('A',
	call_digitalWrite(v('T'),v('Port'),v('ValX')),
	call_digitalWrite(v('T'),v('Port'),v('ValY')),
	ne(v('ValX'),v('ValY'))).

blink0_constraint('B',
	call_pinMode(v('T'),v('Port'),v('ModeX')),
	call_pinMode(v('T'),v('Port'),v('ModeY')),
	ne(v('ModeX'),v('ModeY'))).

blink0_constraint('C',
	turn_on(v('T')),
	turn_off(v('T')),
	true).

blink0_constraint('D',
	turn_on(v('T')),
	delayed_turn_off(v('T'),v('From'),v('Delay')),
	true).

blink0_constraint('E',
	turn_off(v('T')),
	delayed_turn_on(v('T'),v('From'),v('Delay')),
	true).

blink0_constraint('F',
	delayed_turn_on(v('T'),v('FromX'),v('DelayX')),
	delayed_turn_off(v('T'),v('FromY'),v('DelayY')),
	true).

blink0_constraint('G',
	turn_on(v('T')),
	delayed_turn_on(v('T'),v('From'),v('Delay')),
	true).

blink0_constraint('H',
	turn_off(v('T')),
	delayed_turn_off(v('T'),v('From'),v('Delay')),
	true).

blink0_constraint('I',
	delayed_turn_off(v('T'),v('FromX'),v('DelayX')),
	delayed_turn_off(v('T'),v('FromY'),v('DelayY')),
	or(ne(v('FromX'),v('FromY')), ne(v('DelayX'),v('DelayY')))).


blink0_constraint('J',
	delayed_turn_on(v('T'),v('FromX'),v('DelayX')),
	delayed_turn_on(v('T'),v('FromY'),v('DelayY')),
	or(ne(v('FromX'),v('FromY')), ne(v('DelayX'),v('DelayY')))).


%==============================================================================
% Another Version of a Blink Program which currently cannot be verified.
%==============================================================================

% This example is interesting.
% The difference is that turn_on becomes true in the same state
% that contains delayed_turn_on (when the time is reached).
% It needs more general constraints.
% We must specify that turn_on cannot be true at the same time with
% delayed_turn_on as long as the time of delayed_turn_on is not reached.
% We will work on permitting such constraints, too.
% The problem was found by the current implementation,
% so also a negative example like this one has some value.

%------------------------------------------------------------------------------
% blink1_rule(No, Head, BodyList):
%------------------------------------------------------------------------------

% Variables are encoded v(VarName). VarName should not end in a digit.

blink1_rule(1,
	call_pinMode(0,13,output),
	[]).
blink1_rule(2,
	turn_on(1),
	[]).
blink1_rule(3,
	delayed_turn_off(v('S'), v('From'), 1000),
		[turn_on(v('T')),
		ret_millis(v('T'), v('From')),
		succ(v('T'),v('S'))]).
blink1_rule(4,
	delayed_turn_off(v('S'),v('From'),v('Delay')),
		[delayed_turn_off(v('T'),v('From'),v('Delay')),
		ret_millis(v('T'),v('Now')),
		plus_lt(v('From'), v('Delay'), v('Now')),
		succ(v('T'),v('S'))]).
blink1_rule(5,
	turn_off(v('T')),
		[delayed_turn_off(v('T'),v('From'),v('Delay')),
		ret_millis(v('T'),v('Now')),
		plus_ge(v('From'), v('Delay'), v('Now'))]).
blink1_rule(6,
	delayed_turn_on(v('S'),v('From'),1000),
		[turn_off(v('T')),
		ret_millis(v('T'),v('From')),
		succ(v('T'),v('S'))]).
blink1_rule(7,
	delayed_turn_on(v('S'),v('From'),v('Delay')),
		[delayed_turn_on(v('T'),v('From'),v('Delay')),
		ret_millis(v('T'),v('Now')),
		plus_lt(v('From'), v('Delay'), v('Now')),
		succ(v('T'),v('S'))]).
blink1_rule(8,
	turn_on(v('T')),
		[delayed_turn_on(v('T'),v('From'),v('Delay')),
		ret_millis(v('T'),v('Now')),
		plus_ge(v('From'),v('Delay'),v('Now'))]).
blink1_rule(9,
	call_digitalWrite(v('T'), 13, high),
		[turn_on(v('T'))]).
blink1_rule(10,
	call_digitalWrite(v('T'), 13, low),
		[turn_off(v('T'))]).
blink1_rule(11,
	always(0),
	[]).
blink1_rule(12,
	always(v('S')),
		[always(v('T')),
		succ(v('T'),v('S'))]).
blink1_rule(13,
	call_millis(v('T')),
		[always(v('T'))]).

%------------------------------------------------------------------------------
% blink1_constraint(ID, Lit1, Lit2, Formula):
%------------------------------------------------------------------------------

% Variables are encoded v(VarName). VarName should not end in a digit.

blink1_constraint('A',
	call_digitalWrite(v('T'),v('Port'),v('ValX')),
	call_digitalWrite(v('T'),v('Port'),v('ValY')),
	ne(v('ValX'),v('ValY'))).

blink1_constraint('B',
	call_pinMode(v('T'),v('Port'),v('ModeX')),
	call_pinMode(v('T'),v('Port'),v('ModeY')),
	ne(v('ModeX'),v('ModeY'))).

blink1_constraint('C',
	turn_on(v('T')),
	turn_off(v('T')),
	true).

blink1_constraint('D',
	turn_on(v('T')),
	delayed_turn_off(v('T'),v('From'),v('Delay')),
	true).

blink1_constraint('E',
	turn_off(v('T')),
	delayed_turn_on(v('T'),v('From'),v('Delay')),
	true).

blink1_constraint('F',
	delayed_turn_on(v('T'),v('FromX'),v('DelayX')),
	delayed_turn_off(v('T'),v('FromY'),v('DelayY')),
	true).

blink1_constraint('G',
	delayed_turn_off(v('T'),v('FromX'),v('DelayX')),
	delayed_turn_off(v('T'),v('FromY'),v('DelayY')),
	or(ne(v('FromX'),v('FromY')), ne(v('DelayX'),v('DelayY')))).


blink1_constraint('H',
	delayed_turn_on(v('T'),v('FromX'),v('DelayX')),
	delayed_turn_on(v('T'),v('FromY'),v('DelayY')),
	or(ne(v('FromX'),v('FromY')), ne(v('DelayX'),v('DelayY')))).

blink1_constraint('I',
	ret_millis(v('T'),v('NowX')),
	ret_millis(v('T'),v('NowY')),
	ne(v('NowX'),v('NowY'))).

