package AvatarGeneral { 
    public import Base::Anything;
    public import ScalarValues::Positive;
    public import ScalarValues::Integer;
    public import ScalarValues::Boolean;
    public import ScalarValues::String;
    public import ScalarValues::Real;
    public import Occurrences::HappensJustBefore;
    public import SequenceFunctions::*;
    public import Clocks::Clock;
    
    // Assignment =======================================
    action def '#Assignment' {
	    '@target' : Anything[0..*] nonunique;
	    '@value' : Anything[0..*] nonunique;
	    first start; then assign '@target':= '@value'; then done;
    }
    
    // SETS AND RANDOMS =============================================================

    calc '#bound_random' {
        doc /* A primitive to get a random number between two bounds */

        in low : Integer;
        in high : Integer;
        return result: Integer;
        snapshot start redefines start {assert constraint { low <= high }}
        snapshot done redefines done {assert constraint { result >= low & result <= high }}
    }

    calc def '#Unary_predicate' {
        doc /* A unary predicate is a predicate with one single parameter */
        in parameter : Anything;
        return result : Boolean;
    }

    action def '#Unary_action' {
        doc /* A unary action is an action with one single parameter */
        in parameter : Anything;
    }

    calc '#identity' {
        doc /* To build a predicate that tests if a value is equal to another one */
        in tgt : Anything;
        return : '#Unary_predicate' = pred;
        calc pred : '#Unary_predicate' {
            in parameter : Anything redefines parameter;
            return result : Boolean;
            parameter == tgt
        }
    }

    action '#unary_nop' : '#Unary_action' {
        doc /* A unary action that does nothing */
        succession immediate :  HappensJustBefore first start then done;
    }

    calc '#unary_true' : '#Unary_predicate' {
    	doc /* A unary predicate that always return true */
        succession immediate :  HappensJustBefore first start then done;
        assign result := true;
    }

	action '#nop' { doc /* the action which does nothing */ }
	
    action '#multiset_iter' {
        doc
            /* A general purpose tool to iter tests and actions on elements of a multiset represented
            * by an ordered list
            */
        in multiset : Anything[0..*] ordered nonunique;       // the multiset on which to iter
        in pred : '#Unary_predicate'  default '#unary_true';  // to select elements
        in pre_act : '#Unary_action'  default '#unary_nop';   // to apply on all elements, before if_act
        in if_act : '#Unary_action'   default '#unary_nop';   // to apply on selected elements
        in post_act : '#Unary_action'  default '#unary_nop';   // to apply on all elements, after if_act
        out selected : Anything[0..*];                        // all x in s satisfying pred(x)
        out discarded : Anything[0..*];                       // all x in s satisfying not pred(x)
        attribute accepted : Boolean;
        
        first start then iter;
        action iter for i : Positive in 1..multiset -> size() {
            
            first start then select;
            action select 
                if pred(multiset#(i)) { 
                    first start; 
                    then assign accepted := true;
                }
                else { 
                    first start;
                    then assign accepted := false;
                    then assign discarded := (discarded,multiset#(i));
                }
            then do_actions;
            action do_actions {
                first start;
                then action subsets pre_act{ in parameter = multiset#(i); }
                then if accepted { 
                    first start;
                    then action subsets if_act { in parameter = multiset#(i); }
                    then done;
                }
                then action subsets post_act { in parameter = multiset#(i); }
                then done;
            } then done;
        } then done;
    }

    calc '#multiset_random' {
        doc /* A function that randomly returns an element of a (parameter) multiset */
        in multiset : Anything[0..*] ordered; // the set from which an element is expected
        out : Anything[0..1] := if multiset == null? null else multiset#('#bound_random'(1,size(multiset)));
    }
    
    action '#multiset_remove' {
        doc
            /* A tool for removing elements from a multiset */
            
        inout multiset : Anything[0..*] ordered nonunique;       // the multiset to update
        in pred : '#Unary_predicate';  // to select elements to remove
        
        perform action iter subsets '#multiset_iter' {
        	in multiset redefines multiset = multiset;
        	in pred redefines pred = pred;
        }
        then assign multiset := iter.discarded;
    }
    
    calc '#multiset_exists' {
        doc
            /* A tool for testing if some elements of a multiset satisfy a predicate */
            
        in multiset : Anything[0..*] ordered nonunique;       // the multiset to update
        in pred : '#Unary_predicate';  // to select elements to remove
        
        perform action iter subsets '#multiset_iter' {
        	in multiset redefines multiset = multiset;
        	in pred redefines pred = pred;
        }
        iter.selected != null
    }

    // LOCK FOR MUTUAL EXCLUSION ===================================================

    part def '#Lock' {
        doc /* A simple semaphore with size 1, to protect critical sections */
        private attribute locked : Boolean := false;

        action lock {
            doc /* To take the helm. Blocks until the protected ressource is available */
            comment
                /* In this action, assignments actions are atomic, immediate succession s
                * (HappensJustBefore) correctly handles concurrency */
            attribute success : Boolean;
            first start;
            then action wait accept when not locked;
            then action test_lock assign success := not locked;
            succession s : HappensJustBefore first test_lock then do_lock;
            action do_lock assign locked := true;
        }
        
        action unlock {
            doc /* To release the protected ressource */
            first start; then assign locked := false;
        }
    }
    
    // SYSTEM SHARED CLOCK FOR DISCRETE TIME ================================
    
	item '#systemClock' : Clock { 
		doc /* a system level discrete clock to handle delays */
		currentTime : Integer redefines currentTime;
	}
}