Class `Elo_to_SMV_LTL.converter`Source

constraint 'a = Libelectrod__Elo_to_ltl1.stack

method build_Add : Libelectrod__Elo_to_ltl1.stack ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.term

method build_All : Libelectrod__Elo_to_ltl1.stack -> Libelectrod.Elo.quant

method build_And : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method build_Block : Libelectrod__Elo_to_ltl1.stack -> ltl list -> ltl

method build_Card : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  SMV_LTL.term

method build_Compr : Libelectrod__Elo_to_ltl1.stack ->
  (bool * int * Libelectrod.Elo.exp) list ->
  Libelectrod.Elo.fml list ->
  (bool * int * (Libelectrod.Tuple.t -> ltl)) list ->
  ltl list ->
  Libelectrod.Tuple.t ->
  ltl

method build_Diff : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_F : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method build_FIte : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.fml ->
  Libelectrod.Elo.fml ->
  Libelectrod.Elo.fml ->
  ltl ->
  ltl ->
  ltl ->
  ltl

method build_False : Libelectrod__Elo_to_ltl1.stack -> ltl

method build_G : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method build_Gt : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method build_Gte : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method build_H : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method build_IBin : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.iexp ->
  Libelectrod.Elo.ibinop ->
  Libelectrod.Elo.iexp ->
  SMV_LTL.term ->
  (SMV_LTL.term -> SMV_LTL.term -> SMV_LTL.term) ->
  SMV_LTL.term ->
  SMV_LTL.term

method build_IComp : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.iexp ->
  Libelectrod.Elo.icomp_op ->
  Libelectrod.Elo.iexp ->
  SMV_LTL.term ->
  SMV_LTL.tcomp ->
  SMV_LTL.term ->
  ltl

method build_IEq : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method build_INEq : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method build_IUn : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.iunop ->
  Libelectrod.Elo.iexp ->
  (SMV_LTL.term -> SMV_LTL.term) ->
  SMV_LTL.term ->
  SMV_LTL.term

method build_Iden : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Tuple.t ->
  ltl

method build_Iff : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method build_Imp : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method build_In : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method build_Inter : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_Join : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_LBin : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.fml ->
  Libelectrod.Elo.lbinop ->
  Libelectrod.Elo.fml ->
  ltl ->
  (ltl -> ltl -> ltl) ->
  ltl ->
  ltl

method build_LProj : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_LUn : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.lunop ->
  Libelectrod.Elo.fml ->
  (ltl -> ltl) ->
  ltl ->
  ltl

method build_Lt : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method build_Lte : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method build_Name : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Name.t ->
  Libelectrod.Name.t ->
  Libelectrod.Tuple.t ->
  ltl

method build_Neg : Libelectrod__Elo_to_ltl1.stack ->
  SMV_LTL.term ->
  SMV_LTL.term

method build_No : Libelectrod__Elo_to_ltl1.stack -> Libelectrod.Elo.quant

method build_None_ : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Tuple.t ->
  ltl

method build_Not : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method build_NotIn : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method build_Num : Libelectrod__Elo_to_ltl1.stack -> int -> int -> SMV_LTL.term

method build_O : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method build_Or : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method build_Over : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_P : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method build_Prime : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_Prod : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_Quant : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.quant ->
  (bool * int * Libelectrod.Elo.exp) ->
  Libelectrod.Elo.fml list ->
  Libelectrod.Elo.quant ->
  (bool * int * (Libelectrod.Tuple.t -> ltl)) ->
  ltl list ->
  ltl

method build_R : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method build_RBin : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.rbinop ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Elo.exp ->
    Libelectrod.Elo.exp ->
    (Libelectrod.Tuple.t -> ltl) ->
    (Libelectrod.Tuple.t -> ltl) ->
    Libelectrod.Tuple.t ->
    ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_RComp : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.comp_op ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Elo.exp ->
    Libelectrod.Elo.exp ->
    (Libelectrod.Tuple.t -> ltl) ->
    (Libelectrod.Tuple.t -> ltl) ->
    ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method build_REq : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method build_RIte : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.fml ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  ltl ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_RNEq : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method build_RProj : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_RTClos : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_RUn : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.runop ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Elo.exp ->
    (Libelectrod.Tuple.t -> ltl) ->
    Libelectrod.Tuple.t ->
    ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_S : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method build_Some_ : Libelectrod__Elo_to_ltl1.stack -> Libelectrod.Elo.quant

method build_Sub : Libelectrod__Elo_to_ltl1.stack ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.term

method build_TClos : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_Transpose : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_True : Libelectrod__Elo_to_ltl1.stack -> ltl

method build_U : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method build_Union : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_Univ : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Tuple.t ->
  ltl

method build_Var : Libelectrod__Elo_to_ltl1.stack ->
  int ->
  int ->
  Libelectrod.Tuple.t ->
  ltl

method build_X : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method build_oexp : Libelectrod__Elo_to_ltl1.stack ->
  (Libelectrod.Elo.fml, Libelectrod.Elo.exp, Libelectrod.Elo.iexp)
    Libelectrod.Elo.oexp ->
  (Libelectrod.Tuple.t -> ltl) ->
  int ->
  Libelectrod.Tuple.t ->
  ltl

method visit_'exp : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Tuple.t ->
  ltl

method visit_'fml : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.fml ->
  ltl

method visit_'iexp : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.iexp ->
  SMV_LTL.term

method visit_Add : Libelectrod__Elo_to_ltl1.stack ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.term

method visit_All : Libelectrod__Elo_to_ltl1.stack -> Libelectrod.Elo.quant

method visit_And : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method visit_Block : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.fml list ->
  ltl

method visit_Card : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  SMV_LTL.term

method visit_Compr : Libelectrod__Elo_to_ltl1.stack ->
  (bool * int * Libelectrod.Elo.exp) list ->
  Libelectrod.Elo.fml list ->
  Libelectrod.Tuple.t ->
  ltl

method visit_Diff : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_F : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method visit_FIte : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.fml ->
  Libelectrod.Elo.fml ->
  Libelectrod.Elo.fml ->
  ltl

method visit_False : Libelectrod__Elo_to_ltl1.stack -> ltl

method visit_G : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method visit_Gt : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method visit_Gte : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method visit_H : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method visit_IBin : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.iexp ->
  Libelectrod.Elo.ibinop ->
  Libelectrod.Elo.iexp ->
  SMV_LTL.term

method visit_IComp : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.iexp ->
  Libelectrod.Elo.icomp_op ->
  Libelectrod.Elo.iexp ->
  ltl

method visit_IEq : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method visit_INEq : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method visit_IUn : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.iunop ->
  Libelectrod.Elo.iexp ->
  SMV_LTL.term

method visit_Iden : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Tuple.t ->
  ltl

method visit_Iff : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method visit_Imp : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method visit_In : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method visit_Inter : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_Join : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_LBin : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.fml ->
  Libelectrod.Elo.lbinop ->
  Libelectrod.Elo.fml ->
  ltl

method visit_LProj : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_LUn : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.lunop ->
  Libelectrod.Elo.fml ->
  ltl

method visit_Lt : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method visit_Lte : Libelectrod__Elo_to_ltl1.stack -> SMV_LTL.tcomp

method visit_Name : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Name.t ->
  Libelectrod.Tuple.t ->
  ltl

method visit_Neg : Libelectrod__Elo_to_ltl1.stack ->
  SMV_LTL.term ->
  SMV_LTL.term

method visit_No : Libelectrod__Elo_to_ltl1.stack -> Libelectrod.Elo.quant

method visit_None_ : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Tuple.t ->
  ltl

method visit_Not : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method visit_NotIn : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method visit_Num : Libelectrod__Elo_to_ltl1.stack -> int -> SMV_LTL.term

method visit_O : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method visit_Or : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method visit_Over : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_P : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method visit_Prime : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Tuple.t ->
  ltl

method visit_Prod : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_Quant : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.quant ->
  (bool * int * Libelectrod.Elo.exp) ->
  Libelectrod.Elo.fml list ->
  ltl

method visit_R : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method visit_RBin : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.rbinop ->
  Libelectrod.Elo.exp ->
  Libelectrod.Tuple.t ->
  ltl

method visit_RComp : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.comp_op ->
  Libelectrod.Elo.exp ->
  ltl

method visit_REq : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method visit_RIte : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.fml ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  Libelectrod.Tuple.t ->
  ltl

method visit_RNEq : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method visit_RProj : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_RTClos : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_RUn : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.runop ->
  Libelectrod.Elo.exp ->
  Libelectrod.Tuple.t ->
  ltl

method visit_S : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method visit_Some_ : Libelectrod__Elo_to_ltl1.stack -> Libelectrod.Elo.quant

method visit_Sub : Libelectrod__Elo_to_ltl1.stack ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.term

method visit_TClos : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_Transpose : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_True : Libelectrod__Elo_to_ltl1.stack -> ltl

method visit_U : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl -> ltl

method visit_Union : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_Univ : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Tuple.t ->
  ltl

method visit_Var : Libelectrod__Elo_to_ltl1.stack ->
  int ->
  Libelectrod.Tuple.t ->
  ltl

method visit_X : Libelectrod__Elo_to_ltl1.stack -> ltl -> ltl

method visit_comp_op : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.comp_op ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method visit_exp : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Tuple.t ->
  ltl

method visit_fml : Libelectrod__Elo_to_ltl1.stack -> Libelectrod.Elo.fml -> ltl

method visit_ibinop : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.ibinop ->
  SMV_LTL.term ->
  SMV_LTL.term ->
  SMV_LTL.term

method visit_icomp_op : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.icomp_op ->
  SMV_LTL.tcomp

method visit_iexp : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.iexp ->
  SMV_LTL.term

method visit_iunop : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.iunop ->
  SMV_LTL.term ->
  SMV_LTL.term

method visit_lbinop : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.lbinop ->
  ltl ->
  ltl ->
  ltl

method visit_lunop : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.lunop ->
  ltl ->
  ltl

method visit_oexp : Libelectrod__Elo_to_ltl1.stack ->
  (Libelectrod.Elo.fml, Libelectrod.Elo.exp, Libelectrod.Elo.iexp)
    Libelectrod.Elo.oexp ->
  Libelectrod.Tuple.t ->
  ltl

method visit_ofml : Libelectrod__Elo_to_ltl1.stack ->
  (Libelectrod.Elo.fml, Libelectrod.Elo.exp, Libelectrod.Elo.iexp)
    Libelectrod.Elo.ofml ->
  ltl

method visit_oiexp : Libelectrod__Elo_to_ltl1.stack ->
  (Libelectrod.Elo.fml, Libelectrod.Elo.exp, Libelectrod.Elo.iexp)
    Libelectrod.Elo.oiexp ->
  SMV_LTL.term

method visit_prim_oexp : Libelectrod__Elo_to_ltl1.stack ->
  (Libelectrod.Elo.fml, Libelectrod.Elo.exp, Libelectrod.Elo.iexp)
    Libelectrod.Elo.prim_oexp ->
  Libelectrod.Tuple.t ->
  ltl

method visit_quant : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.quant ->
  Libelectrod.Elo.quant

method visit_rbinop : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.rbinop ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_runop : Libelectrod__Elo_to_ltl1.stack ->
  Libelectrod.Elo.runop ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

Install

Dune Dependency

Authors

Maintainers

Sources

doc/electrod.libelectrod/Libelectrod/Elo_to_smv1/Elo_to_SMV_LTL/class-converter/index.html

Class `Elo_to_SMV_LTL.converter`Source

package electrod

Install

Dune Dependency

Authors

Maintainers

Sources

doc/electrod.libelectrod/Libelectrod/Elo_to_smv1/Elo_to_SMV_LTL/class-converter/index.html

Class Elo_to_SMV_LTL.converterSource

Class `Elo_to_SMV_LTL.converter`Source