program leader;

import java.lang.System;

define(progress_timer_start, keys(0), {Long});
progress_timer_start(1000L);

define(last_installed, keys(0), {String, Integer});
define(my_start, {String, Integer});

timer(seconds, physical, 1000, infinity, 0);

define(start, keys(0), {String});

public
my_start(Me, Id) :-
    start(),
    paxos::parliament(Me, Him, Id),
    Me == Him;

/*********** progress_timer block **************/
define(progress_timer, keys(0), {String, Long, Long});

public
progress_timer(Me, -1, Duration) :-
    my_start(Me, _),
    progress_timer_start(Duration);

progress_timer(Me, Start, NewDuration) :-
    preinstall(Me, _),
    progress_timer(Me, _, Duration),
    Start := System.currentTimeMillis()
{
    NewDuration := Duration * 2;
    //System.out.println("\tDouble progress timer to " + NewDuration.toString());
};

progress_timer(Me, Start, StartDur) :-
    progress_timer(Me, _, Duration),
    progress_timer_start(StartDur),
    do_election(Me, _, _),
    Start := System.currentTimeMillis();
/*********** END progress_timer block **************/

/*********** do_election block **************/
define(do_election, {String, Integer, String});

public
do_election(Me, Id, Me) :-
    my_start(Me, Id);

/* safety-critical logic is (perhaps inappropriately) 
   defined here: do_election carries with it the new View number.
*/
do_election(Me, Id, Me) :-
    progress_timer(Me, Start, Duration),
    seconds#insert(),
    last_attempted(Me, Last),
    paxos::priestCnt(Me, Cnt),
    Id := Last + Cnt,
    Start != -1,
    (System.currentTimeMillis() - Start) > Duration;


/* if progress timer isn't set, and View > Last */
do_election(Me, View, Originator) :-
    view_change(Me, View, Other, Originator),
    last_attempted(Me, Last),
    Me != Other,
    View > Last;
    /* the progress_timer rule doesn't seem to work.  relaxing it; may 
       cause livelock issues
    progress_timer(Me, _, StartDuration),
    progress_timer_start(StartDuration);
    */


/*********** END do_election block **************/


/*********** last_attempted block **************/
define(last_attempted, keys(0), {String, Integer});

/* define start states! */
public
last_attempted(Me, Id) :-
    my_start(Me, Id);

// I think that with bug Z out of the way, we can make this jump
last_attempted(Me, Id) :-
    do_election(Me, Id, Me2),
    last_attempted(Me, OldId),
    paxos::priestCnt(Me, Cnt),
    Me == Me2,
    OldId < Id
{
	New := OldId + Cnt;
	//System.out.println(Me.toString() + " = " + Me2.toString() + " -- OUCH: " + OldId.toString() + " to "+ New.toString());
};

/*********** END last_attempted block **************/


/*********** view_change block **************/
define(view_change, keys(0, 1, 2), {String, Integer, String, String});
view_change(@Other, Id, Me, Originator) :-
    do_election(@Me, Id, Originator),
    paxos::parliament(@Me, Other, _);


define(vc_cnt, keys(0, 1), {String, Integer, Integer});
vc_cnt(Me, View, count<Other>) :-
    view_change(Me, View, Other, _);

delete
view_change(Me, Id, Other, Orig) :-
    view_change(Me, Id, Other, Orig),
    vc_proof(Me, Id, Other2);

/*********** END view_change block **************/
define(preinstall, {String, Integer});
preinstall(Me, View) :-
    vc_cnt(Me, View, Cnt),
    paxos::priestCnt(Me, Total),
    Cnt > (Total / 2);

// paa hack
define(leader, keys(0, 1), {String, String, Integer});
leader(Me, Originator, View) :-
    preinstall(Me, View),
    view_change(Me, View, _, Originator);

delete
leader(Me, Leader, View) :-
    leader(Me, Leader, View),
    bump_vc_proof(Me, NV),
    NV > View;

public
last_installed(Me, -1) :-
    my_start(Me, _);

last_installed(Me, View) :-
    last_installed(Me, OldView),
    leader#insert(Me, _, View),
    View >= OldView;

/** PROOF MESSAGE STUFF ***/
timer(proof_timer, physical, 2000, infinity, 0);
define(proof_doping, {String, Integer, String});

proof_doping(Me, View, Other) :-
    proof_timer#insert(),
    paxos::parliament(Me, Other),
    last_installed(Me, View);
   
define(vc_proof, {String, Integer, String});
vc_proof(@Other, View, Me) :-
    proof_doping(@Me, View, Other);

define(bump_vc_proof, {String, Integer});
bump_vc_proof(Me, View) :-
    vc_proof(Me, View, Other),
    last_installed(Me, LastI),
    View > LastI;

bump_vc_proof(Me, View) :-
    vc_proof(Me, View, Other),
    notin last_installed(Me, _);