/*
        General Framework for
        State Space Exploration Program

        Module explore.c, Revision 2.0, Date 1996-08-19
*/
#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include "explore.h"
#include "problem.h"

/*
        explore.h defines the bag ADT and the types

    state_index_t    - states are indexed by this type
    bag_of_state_index_t - a bag of state indexes
    bag_of_bag_of_state_index_t - a bag of bags of state indexes

    The specific details of the problem are defined in problem.h 
and problem.c, which must provide:

    NUM_SYS_STATES    - we assume that the state set Q can be indexed by
                    ints (aka state_index_t) 0 ... NUM_SYS_STATES-1

    int target[NUM_SYS_STATES] - the target set for the problem, where 
        target[q_i] = 1 if state q_i is in the target set
                      0 otherwise

    bag_of_bag_of_state_index_t sigma[NUM_SYS_STATES] - the schedular 
        choice fuction. The scheduling demon can take any of the actions 
        in sigma(q), where

        q is the current state
        q_i - current state index. 
              Notationally, _i means the index of a state.
        sigma[q_i] is the entry corresponding to sigma(q)  
        sigma[q_i].card - number of different scheduling choices 
        sigma[q_i].item[j] - choice j
        sigma[q_i].item[j].card - number of possible sys states resulting 
                        from choice j
        sigma[q_i].item[j].item[k] - k'th possible result state of 
                        choice j

    char* state_index_to_str(state_index_t s_i) - a conversion function 
        to convert a state index into a printable string

    int compute_sigma(void) - a function to compute the sigma table,
        returning 1 if ok, 0 if some error occurred.

    int compute_target(void) - a function to compute the target set, 
        returning 1 if ok, 0 if some error occurred.

This code then computes the avoidance probabilities 

    p[q][i] is the probability that, starting in state q, the schedular
        can avoid the target set for at least i steps.

and the path length estimates

    l[q] is (an estimate of) the expected length of a path, that starting 
        at q avoids the target set.
*/

double p[NUM_SYS_STATES][NUM_SYS_STATES+1];
double l[NUM_SYS_STATES];


int verify_no_deadlock(void) {
/*
    Verify that every state has at least one progress making successor,
    and print those that do not.
    
    Pre: sigma is well-defined
    Post: verify_no_deadlock() is
        1 - if OK
        0 - if one or more states deadlock
    Side Effects: prints the states that result in deadlock.
*/
    int q_i;
    int no_deadlock = 1;

    printf("Checking for deadlock states.\n");

    for (q_i=0; q_i < NUM_SYS_STATES; q_i++ ) {
        if ( sigma[q_i].card <= 0 ) {
            printf("State %d deadlocks\n", q_i);
            no_deadlock = 0;
        }
    }
    if ( no_deadlock ) {
        printf("All states are deadlock free.\n\n");
    } else {
        printf("NOT all states are deadlock free.\n\n");
    }

    return no_deadlock;
}


void compute_avoidance_probs(void) {
/*
        Compute avoidance probabilities and determine self-stabilization

        as per Prop 2.5, Prop 2.11, and Theorem 2.10

    Pre: sigma is well-defined
         target is well-defined
    Post: none
    Side Effects:
        -computes p[q_i][n] for each q and for 0 <= n <= NUM_SYS_STATES
        -determines upper bound on expected value of the length of an
        avoiding path
        -determines whether system is self-stabilizing or not
*/
    int q_i;
    int iter_num;

    /* initial probabilities and expected avoidance path lengths */
    for (q_i=0; q_i < NUM_SYS_STATES; q_i++ ) {
        if ( target[q_i] ) {
            /* in the target set, cannot avoid */
            p[q_i][0] = 0.0;    
        } else {
            /* outside target set, can avoid for 0 steps */
            p[q_i][0] = 1.0;    
        }
        l[q_i] = 0.0;
    }

    /* compute p[iter_num] for 0 ... NUM_SYS_STATES */
    for ( iter_num = 0; iter_num < NUM_SYS_STATES; iter_num++ ) {

        for (q_i=0; q_i < NUM_SYS_STATES; q_i++ ) {
            double max_prob = 0.0;

            /* compute maximum over all successors */

            /* if no scheduling choices, prob is constant, equals p[q_i][0] */
            if ( sigma[q_i].card == 0 ) {
                p[q_i][iter_num+1] = p[q_i][0];
            } else {
                int item_num;

                /* sum over scheduling choices */
                for (item_num=0; item_num < sigma[q_i].card; item_num++) {
                    int sys_item_num;
                    double succ_prob = 0;
                    int i;

                    /* each scheduling choice must result in at least 
                       one next state! */
                    assert( sigma[q_i].item[item_num].card != 0 );

                    /* sum over next states for the choice */
                    for (sys_item_num=0; 
                             sys_item_num < sigma[q_i].item[item_num].card;
                             sys_item_num++) 
                    {
                            i = sigma[q_i].item[item_num].item[sys_item_num];
                            succ_prob += p[i][iter_num];
                    }       
                    succ_prob = succ_prob / 
                            ( (double) sigma[q_i].item[item_num].card );
                    max_prob = MAX(max_prob, succ_prob);
                }
                p[q_i][iter_num+1] = max_prob;
            }
        }

        /* update expected length */
        for (q_i=0; q_i < NUM_SYS_STATES; q_i++ ) {
            l[q_i] += ( (double) iter_num ) * p[q_i][iter_num] *
                (1.0 - p[q_i][iter_num+1] );
        }
    }

    /* update tail estimates */
    {
        double pmax = 0;
        double exp_len_max = 0;
        double exp_len_sum = 0;
        double n = NUM_SYS_STATES;
        double tail;

        for (q_i=0; q_i < NUM_SYS_STATES; q_i++ ) {
            pmax = MAX(pmax, p[q_i][NUM_SYS_STATES]);
        }
        tail = n * pmax * ( -1.0 - n * pmax + 3.0 * n + pmax) /
               (2 * (1-pmax) * (1-pmax));

        for (q_i=0; q_i < NUM_SYS_STATES; q_i++ ) {
            /* add in tail only if prob non-zero */
            if ( p[q_i][NUM_SYS_STATES] > 0.0 ) {
                l[q_i] += tail;
            }
            exp_len_sum += l[q_i];
            exp_len_max = MAX(exp_len_max, l[q_i]);
        }

        printf("Number of states, n = %d\n", (int) n);
        printf("Max over q of p_n(q) = %g\n", pmax);
        printf("Upper bound on tail of expected length, l(q) = %g\n", tail);
        printf("Maximum over q of l(q) = %g\n", exp_len_max);
        printf("Average over q of l(q) = %g\n", exp_len_sum/n);
        if ( pmax < 1.0 ) {
            printf("System is self stabilizing.\n");
        } else {
            printf("WARNING: System is NOT self stabilizing.\n");
        }
    }
}


void print_details(void) {
/*
        Print out details of
        sigma 
        expected path lengths
        avoiding probabilities

        Pre: sigma, target, p must be well-defined
*/
    int q_i;

    printf("Computation details:\n");
    printf("q p_n(q) l(q) sigma(q)\n");

    for (q_i=0; q_i < NUM_SYS_STATES; q_i++ ) {
        printf("%s %8.2g %5.1f", 
                state_index_to_str(q_i),
                p[q_i][NUM_SYS_STATES], l[q_i]);
        {
            int item_num;
            int sys_item_num;

            for (item_num=0; item_num < sigma[q_i].card; item_num++) {
                if ( sigma[q_i].item[item_num].card <= 0 ) {
                    printf("item %d is empty!\n", item_num);
                }
                printf(" {");
                for (sys_item_num=0; 
                     sys_item_num < sigma[q_i].item[item_num].card;
                     sys_item_num++) 
                {
                    int qn_i;
                    qn_i = sigma[q_i].item[item_num].item[sys_item_num];

                    printf("%s", state_index_to_str(qn_i));
                    if ( sys_item_num+1 < sigma[q_i].item[item_num].card){
                        printf(", ");
                    }
                }
                printf("}");
            }
        }
        printf("\n");
    }
    printf("\n");
}


void main(int argc, char* argv[]) {

    if ( ! compute_sigma() ) exit(0);

    if ( ! verify_no_deadlock() ) exit(0);
    
    if ( ! compute_target() ) exit(0);

    compute_avoidance_probs();

    /* uncomment the following to see details of the avoidance probs */
    /* print_details(); */
}