// **************************************************************************
//
//    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
//
// **************************************************************************

module Monotonicity(bool ?a1,?a2,?b1,?b2)  {
    nothing;
} satisfies {
    MonoX : assert A (G((a1->a2)&(b1->b2)) -> G((X a1) -> (X a2))) ;
    MonoG : assert A (G((a1->a2)&(b1->b2)) -> G((G a1) -> (G a2))) ;
    MonoF : assert A (G((a1->a2)&(b1->b2)) -> G((F a1) -> (F a2))) ;
    MonoWU : assert A (G((a1->a2)&(b1->b2)) -> G([a1 WU b1] -> [a2 WU b2])) ;
    MonoSU : assert A (G((a1->a2)&(b1->b2)) -> G([a1 SU b1] -> [a2 SU b2])) ;
    //  MonoWW : A (G((a1->a2)&(b1->b2)) -> G([a1 WW b1] -> [a2 WW b2])) ;
    //  MonoSW : A (G((a1->a2)&(b1->b2)) -> G([a1 SW b1] -> [a2 SW b2])) ;
    MonoWB : assert A (G((a1->a2)&(b1->b2)) -> G([a1 WB b2] -> [a2 WB b1])) ;
    MonoSB : assert A (G((a1->a2)&(b1->b2)) -> G([a1 SB b2] -> [a2 SB b1])) ;
}