// ************************************************************************** //
//                                                                            //
//    eses                   eses                                             //
//   eses                     eses                                            //
//  eses    eseses  esesese    eses   Embedded Systems Group                  //
//  ese    ese  ese ese         ese                                           //
//  ese    eseseses eseseses    ese   Department of Computer Science          //
//  eses   eses          ese   eses                                           //
//   eses   eseses  eseseses  eses    University of Kaiserslautern            //
//    eses                   eses                                             //
//                                                                            //
// ************************************************************************** //
//  Elevator Disk Scheduling Algorithm                                        //
// ************************************************************************** //

macro size = 8;

module Elevator(bv{size} ?request, position, event !up, !down) {
    bv{size} requests,
    bv{size} upward_mask,
    bv{size} downward_mask;
    // initialise the position: 00...01
    position = {false::(size-1)}@true;
    // initialise the upward requests mask: 11...10
    upward_mask = not(position);
    // initialise the downward requests mask: 00...00
    downward_mask = {false::size};

    // insert new requests, the current position can be served immediately

    always
        next(requests) = requests & (!position) | request;
||
    // *** head control thread ***
    loop {
        // upward movement ...
        abort
            loop
                // move the head of the disk to the left
                let(next_position = position{-2:}@false) {
                    pause;
                    emit(up);
                    // update the position and the requests masks
                    next(position) = next_position;
                    next(upward_mask) = upward_mask & (!next_position);
                    next(downward_mask) = downward_mask | position;
                }
        // ... until there are no upward requests left
        when( (requests & upward_mask) == {false::(size)});

        // downward movement ...
        abort
            loop
                // move the head of the disk to the right
                let( next_position = false @ position{:1} ) {
                    ell_moving_down: pause;
                    emit(down);
                    // update the position and the requests masks
                    next(position) = next_position;
                    next(upward_mask) = upward_mask | position;
                    next(downward_mask) = downward_mask & (!next_position);
                }
        // ... until there are no upward requests left
        when ( (requests & downward_mask) == {false::(size)});
    }
}
satisfies {
    // the head is not moved below the lower boundary
    head_movement_down : assert A G (position == {false::(size-1)} @ true) -> !down;
    // the head is not moved above the upper boundary
    head_movement_up   : assert A G (position == true @ {false::(size-1)}) -> !up;
    // all requests are eventually served
    requests_served : assert A G forall(i=0 .. (size-1)) (request{i} -> A F position{i});
}