pickupdelivery.cfg

#-----------------------------------------------------------------------
# File: pickupdelivery.cfg
# Date: 01.10.2020
# Athr: M. Khaled
#-----------------------------------------------------------------------

project_name = "pickupdelivery";

system {
    states {
        dimension = "3";
        first_symbol = "0.0,0.0,0.0";
        last_symbol = "15.0,10.0,99.0";
        quantizers = "1.0,1.0,1.0";
        initial_set = "[7.0,7.0]x[5.0,5.0]x[99.0,99.0]";

        subsets {
            names = "pickup1, pickup2, delivery1, delivery2, charger, obstacles, lowbattery, fullbattery";
	    
            mapping_pickup1 = "[-0.5,1.5] x [8.5,9.5] x [-0.5,100.5]";
            mapping_pickup2 = "[13.5,15.5] x [8.5,9.5] x [-0.5,100.5]";
            mapping_delivery1 = "[13.5,15.5] x [0.5,1.5] x [-0.5,100.5]";
            mapping_delivery2 = "[-0.5,1.5] x [0.5,1.5] x [-0.5,100.5]";
            mapping_charger = "[6.5,8.5] x [3.5,4.5] x [-0.5,100.5]";
            mapping_obstacles = "[3.5,15.5] x [2.5,3.5] x [-0.5,100.5] U [-0.5,11.5] x [6.5,7.5] x [-0.5,100.5]";
            mapping_lowbattery = "[-0.5,15.5] x [-0.5,10.5] x [-0.5,9.5]";
            mapping_fullbattery = "[-0.5,15.5] x [-0.5,10.5] x [98.5,99.5]";
        }
    }
    controls {
        dimension = "1";
        first_symbol = "0.0";
        last_symbol = "4.0";
        quantizers = "1.0";
    }
    dynamics {
        step_time = "0.1";
        code_file = "pickupdelivery.cl";
    }
}

specifications {
    ltl_formula = "G(!obstacles) & GF(pickup1) & GF(pickup2) & G(pickup1->((!charger & !pickup2 &  !delivery2) U delivery1)) & G(pickup2->((!charger & !pickup1 &  !delivery1) U delivery2)) & G(lowbattery -> (charger U fullbattery))";
}

implementation {
    type = "mealy_machine";
    generate_controller = "true";
}

simulation {
    window_width = "1200";
    window_height = "600";
    widow_title = "Pickup-Delivery Drone Example";
    initial_state = "7.0,5.0,99.0";
    controller_file = "pickupdelivery.mdf";
    system_image = "drone.png";
    system_image_scale = "0.1";
    use_ode = "false";
    visualize_3rdDim = "false";
    skip_APs = "lowbattery,fullbattery";
    path_tail_length = "10";
}