Source file Smv_trace_parser.ml

module Make

# 15 "src/Smv_trace_parser.mly"
           (D : sig
  val base : (Name.t, Tuple_set.t) CCList.Assoc.t 
end)
# 9 "src/Smv_trace_parser.ml"

= struct
  
  module MenhirBasics = struct
    
    exception Error
    
    let _eRR =
      fun _s ->
        raise Error
    
    type token = Smv_trace_tokens.token
    
  end
  
  include MenhirBasics
  
# 19 "src/Smv_trace_parser.mly"
  

(* fixes issue between Menhir and dune *)
(* https://github.com/ocaml/dune/issues/2450 *)
module Libelectrod = struct end  

  open Containers

  (* vendored from Containers (BSD license allows this): 
    its prototype changd in 2.4, so copy a version to
    compile with many versions of Containers.  *)
  let rec search_set eq acc l x ~f = match l with
    | [] -> f x None acc
    | (x',y')::l' ->
      if eq x x'
      then f x (Some y') (List.rev_append acc l')
      else search_set eq ((x',y')::acc) l' x ~f

  let update ~eq f x l =
    search_set eq [] l x
      ~f:(fun x opt_y rest ->
        match f opt_y with
          | None -> rest (* drop *)
          | Some y' -> (x,y') :: rest)
  (* END vendoring *)

  
  (* converts a list containing pairs (name, tuple) in a list of pairs (name,
     set of tuples), i.e. gathers (in [acc]) all tuples corresponding to a given
     name in a same set. The list is nonempty. *)
  let upd tuple = function
    | None -> Some (Tuple_set.singleton tuple)
    | Some ts -> Some (Tuple_set.add tuple ts)
    
  let convert_name_tuple_l ntl =
    let rec walk acc = function
      | [] -> acc
      (* if None: means that atom was FALSE, else TRUE *)
      | None::tl -> walk acc tl
      | Some (name, tuple)::tl ->
         begin
           (* Msg.debug (fun m -> m "conv (%a, %a)" Name.pp name Tuple.pp tuple); *)
           let acc2 = update ~eq:Name.equal (upd tuple) name acc in
           walk acc2 tl
         end
    in walk D.base ntl


  (* From what we gathered, we should remove the last state from the returned
     trace (it is the loop-target state), and if the first state is the target,
     it is not said so we have to tag it as a loop-target by ourselves. *)
  let met_one_loop = ref false

  let rec remove_last = function
    | [] -> assert false
    | [_] -> []
    | hd::tl -> hd :: remove_last tl
    
       

# 88 "src/Smv_trace_parser.ml"
  
  type ('s, 'r) _menhir_state = 
    | MenhirState00 : ('s, _menhir_box_trace) _menhir_state
      (** State 00.
        Stack shape : .
        Start symbol: trace. *)

    | MenhirState01 : (('s, _menhir_box_trace) _menhir_cell1_STATE, _menhir_box_trace) _menhir_state
      (** State 01.
        Stack shape : STATE.
        Start symbol: trace. *)

    | MenhirState07 : (('s, _menhir_box_trace) _menhir_cell1_atomic, _menhir_box_trace) _menhir_state
      (** State 07.
        Stack shape : atomic.
        Start symbol: trace. *)

    | MenhirState10 : (('s, _menhir_box_trace) _menhir_cell1_LOOP, _menhir_box_trace) _menhir_state
      (** State 10.
        Stack shape : LOOP.
        Start symbol: trace. *)

    | MenhirState13 : (('s, _menhir_box_trace) _menhir_cell1_state, _menhir_box_trace) _menhir_state
      (** State 13.
        Stack shape : state.
        Start symbol: trace. *)

  
  and ('s, 'r) _menhir_cell1_atomic = 
    | MenhirCell1_atomic of 's * ('s, 'r) _menhir_state * ((Name.t * Tuple.t) option)
  
  and ('s, 'r) _menhir_cell1_state = 
    | MenhirCell1_state of 's * ('s, 'r) _menhir_state * (Outcome.state)
  
  and ('s, 'r) _menhir_cell1_LOOP = 
    | MenhirCell1_LOOP of 's * ('s, 'r) _menhir_state
  
  and ('s, 'r) _menhir_cell1_STATE = 
    | MenhirCell1_STATE of 's * ('s, 'r) _menhir_state
  
  and _menhir_box_trace = 
    | MenhirBox_trace of (Outcome.states) [@@unboxed]
  
  let _menhir_action_01 =
    fun () ->
      (
# 105 "src/Smv_trace_parser.mly"
    ( None )
# 137 "src/Smv_trace_parser.ml"
       : ((Name.t * Tuple.t) option))
  
  let _menhir_action_02 =
    fun v ->
      (
# 107 "src/Smv_trace_parser.mly"
    ( Some v )
# 145 "src/Smv_trace_parser.ml"
       : ((Name.t * Tuple.t) option))
  
  let _menhir_action_03 =
    fun () ->
      (
# 216 "<standard.mly>"
    ( [] )
# 153 "src/Smv_trace_parser.ml"
       : ((Name.t * Tuple.t) option list))
  
  let _menhir_action_04 =
    fun x xs ->
      (
# 219 "<standard.mly>"
    ( x :: xs )
# 161 "src/Smv_trace_parser.ml"
       : ((Name.t * Tuple.t) option list))
  
  let _menhir_action_05 =
    fun x ->
      (
# 228 "<standard.mly>"
    ( [ x ] )
# 169 "src/Smv_trace_parser.ml"
       : (Outcome.state list))
  
  let _menhir_action_06 =
    fun x xs ->
      (
# 231 "<standard.mly>"
    ( x :: xs )
# 177 "src/Smv_trace_parser.ml"
       : (Outcome.state list))
  
  let _menhir_action_07 =
    fun ntl ->
      let loop = 
# 115 "src/Smv_trace_parser.mly"
( false )
# 185 "src/Smv_trace_parser.ml"
       in
      (
# 94 "src/Smv_trace_parser.mly"
    (
      let valu = Outcome.valuation @@ convert_name_tuple_l ntl in
      if loop && not !met_one_loop then (* nuXmv may report several loop states, we only keep one *)
        (met_one_loop := true;
         Outcome.loop_state valu)
      else
        Outcome.plain_state valu
    )
# 197 "src/Smv_trace_parser.ml"
       : (Outcome.state))
  
  let _menhir_action_08 =
    fun ntl ->
      let loop = 
# 117 "src/Smv_trace_parser.mly"
    ( true )
# 205 "src/Smv_trace_parser.ml"
       in
      (
# 94 "src/Smv_trace_parser.mly"
    (
      let valu = Outcome.valuation @@ convert_name_tuple_l ntl in
      if loop && not !met_one_loop then (* nuXmv may report several loop states, we only keep one *)
        (met_one_loop := true;
         Outcome.loop_state valu)
      else
        Outcome.plain_state valu
    )
# 217 "src/Smv_trace_parser.ml"
       : (Outcome.state))
  
  let _menhir_action_09 =
    fun states ->
      (
# 88 "src/Smv_trace_parser.mly"
    (
      remove_last states
    )
# 227 "src/Smv_trace_parser.ml"
       : (Outcome.states))
  
  let _menhir_print_token : token -> string =
    fun _tok ->
      match _tok with
      | Smv_trace_tokens.ATOMIC _ ->
          "ATOMIC"
      | Smv_trace_tokens.EOF ->
          "EOF"
      | Smv_trace_tokens.EQUAL ->
          "EQUAL"
      | Smv_trace_tokens.FALSE ->
          "FALSE"
      | Smv_trace_tokens.LOOP ->
          "LOOP"
      | Smv_trace_tokens.STATE ->
          "STATE"
      | Smv_trace_tokens.TRUE ->
          "TRUE"
  
  let _menhir_fail : unit -> 'a =
    fun () ->
      Printf.eprintf "Internal failure -- please contact the parser generator's developers.\n%!";
      assert false
  
  include struct
    
    [@@@ocaml.warning "-4-37"]
    
    let _menhir_run_15 : type  ttv_stack. ttv_stack -> _ -> _menhir_box_trace =
      fun _menhir_stack _v ->
        let states = _v in
        let _v = _menhir_action_09 states in
        MenhirBox_trace _v
    
    let rec _menhir_goto_nonempty_list_state_ : type  ttv_stack. ttv_stack -> _ -> (ttv_stack, _menhir_box_trace) _menhir_state -> _menhir_box_trace =
      fun _menhir_stack _v _menhir_s ->
        match _menhir_s with
        | MenhirState00 ->
            _menhir_run_15 _menhir_stack _v
        | MenhirState13 ->
            _menhir_run_14 _menhir_stack _v
        | _ ->
            _menhir_fail ()
    
    and _menhir_run_14 : type  ttv_stack. (ttv_stack, _menhir_box_trace) _menhir_cell1_state -> _ -> _menhir_box_trace =
      fun _menhir_stack _v ->
        let MenhirCell1_state (_menhir_stack, _menhir_s, x) = _menhir_stack in
        let xs = _v in
        let _v = _menhir_action_06 x xs in
        _menhir_goto_nonempty_list_state_ _menhir_stack _v _menhir_s
    
    let rec _menhir_run_01 : type  ttv_stack. ttv_stack -> _ -> _ -> (ttv_stack, _menhir_box_trace) _menhir_state -> _menhir_box_trace =
      fun _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s ->
        let _menhir_stack = MenhirCell1_STATE (_menhir_stack, _menhir_s) in
        let _tok = _menhir_lexer _menhir_lexbuf in
        match (_tok : MenhirBasics.token) with
        | Smv_trace_tokens.ATOMIC _v ->
            _menhir_run_02 _menhir_stack _menhir_lexbuf _menhir_lexer _v MenhirState01
        | Smv_trace_tokens.EOF | Smv_trace_tokens.LOOP | Smv_trace_tokens.STATE ->
            let _v = _menhir_action_03 () in
            _menhir_run_06 _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok
        | _ ->
            _eRR ()
    
    and _menhir_run_02 : type  ttv_stack. ttv_stack -> _ -> _ -> _ -> (ttv_stack, _menhir_box_trace) _menhir_state -> _menhir_box_trace =
      fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s ->
        let _tok = _menhir_lexer _menhir_lexbuf in
        match (_tok : MenhirBasics.token) with
        | Smv_trace_tokens.EQUAL ->
            let _tok = _menhir_lexer _menhir_lexbuf in
            (match (_tok : MenhirBasics.token) with
            | Smv_trace_tokens.TRUE ->
                let _tok = _menhir_lexer _menhir_lexbuf in
                let v = _v in
                let _v = _menhir_action_02 v in
                _menhir_goto_atomic _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
            | Smv_trace_tokens.FALSE ->
                let _tok = _menhir_lexer _menhir_lexbuf in
                let _v = _menhir_action_01 () in
                _menhir_goto_atomic _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
            | _ ->
                _eRR ())
        | _ ->
            _eRR ()
    
    and _menhir_goto_atomic : type  ttv_stack. ttv_stack -> _ -> _ -> _ -> (ttv_stack, _menhir_box_trace) _menhir_state -> _ -> _menhir_box_trace =
      fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok ->
        let _menhir_stack = MenhirCell1_atomic (_menhir_stack, _menhir_s, _v) in
        match (_tok : MenhirBasics.token) with
        | Smv_trace_tokens.ATOMIC _v_0 ->
            _menhir_run_02 _menhir_stack _menhir_lexbuf _menhir_lexer _v_0 MenhirState07
        | Smv_trace_tokens.EOF | Smv_trace_tokens.LOOP | Smv_trace_tokens.STATE ->
            let _v_1 = _menhir_action_03 () in
            _menhir_run_08 _menhir_stack _menhir_lexbuf _menhir_lexer _v_1 _tok
        | _ ->
            _eRR ()
    
    and _menhir_run_08 : type  ttv_stack. (ttv_stack, _menhir_box_trace) _menhir_cell1_atomic -> _ -> _ -> _ -> _ -> _menhir_box_trace =
      fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok ->
        let MenhirCell1_atomic (_menhir_stack, _menhir_s, x) = _menhir_stack in
        let xs = _v in
        let _v = _menhir_action_04 x xs in
        _menhir_goto_list_atomic_ _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
    
    and _menhir_goto_list_atomic_ : type  ttv_stack. ttv_stack -> _ -> _ -> _ -> (ttv_stack, _menhir_box_trace) _menhir_state -> _ -> _menhir_box_trace =
      fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok ->
        match _menhir_s with
        | MenhirState10 ->
            _menhir_run_11 _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok
        | MenhirState07 ->
            _menhir_run_08 _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok
        | MenhirState01 ->
            _menhir_run_06 _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok
        | _ ->
            _menhir_fail ()
    
    and _menhir_run_11 : type  ttv_stack. (ttv_stack, _menhir_box_trace) _menhir_cell1_LOOP -> _ -> _ -> _ -> _ -> _menhir_box_trace =
      fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok ->
        let MenhirCell1_LOOP (_menhir_stack, _menhir_s) = _menhir_stack in
        let ntl = _v in
        let _v = _menhir_action_08 ntl in
        _menhir_goto_state _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
    
    and _menhir_goto_state : type  ttv_stack. ttv_stack -> _ -> _ -> _ -> (ttv_stack, _menhir_box_trace) _menhir_state -> _ -> _menhir_box_trace =
      fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok ->
        match (_tok : MenhirBasics.token) with
        | Smv_trace_tokens.STATE ->
            let _menhir_stack = MenhirCell1_state (_menhir_stack, _menhir_s, _v) in
            _menhir_run_01 _menhir_stack _menhir_lexbuf _menhir_lexer MenhirState13
        | Smv_trace_tokens.LOOP ->
            let _menhir_stack = MenhirCell1_state (_menhir_stack, _menhir_s, _v) in
            _menhir_run_09 _menhir_stack _menhir_lexbuf _menhir_lexer MenhirState13
        | Smv_trace_tokens.EOF ->
            let x = _v in
            let _v = _menhir_action_05 x in
            _menhir_goto_nonempty_list_state_ _menhir_stack _v _menhir_s
        | _ ->
            _menhir_fail ()
    
    and _menhir_run_09 : type  ttv_stack. ttv_stack -> _ -> _ -> (ttv_stack, _menhir_box_trace) _menhir_state -> _menhir_box_trace =
      fun _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s ->
        let _menhir_stack = MenhirCell1_LOOP (_menhir_stack, _menhir_s) in
        let _tok = _menhir_lexer _menhir_lexbuf in
        match (_tok : MenhirBasics.token) with
        | Smv_trace_tokens.STATE ->
            let _tok = _menhir_lexer _menhir_lexbuf in
            (match (_tok : MenhirBasics.token) with
            | Smv_trace_tokens.ATOMIC _v ->
                _menhir_run_02 _menhir_stack _menhir_lexbuf _menhir_lexer _v MenhirState10
            | Smv_trace_tokens.EOF | Smv_trace_tokens.LOOP | Smv_trace_tokens.STATE ->
                let _v = _menhir_action_03 () in
                _menhir_run_11 _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok
            | _ ->
                _eRR ())
        | _ ->
            _eRR ()
    
    and _menhir_run_06 : type  ttv_stack. (ttv_stack, _menhir_box_trace) _menhir_cell1_STATE -> _ -> _ -> _ -> _ -> _menhir_box_trace =
      fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok ->
        let MenhirCell1_STATE (_menhir_stack, _menhir_s) = _menhir_stack in
        let ntl = _v in
        let _v = _menhir_action_07 ntl in
        _menhir_goto_state _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
    
    let _menhir_run_00 : type  ttv_stack. ttv_stack -> _ -> _ -> _menhir_box_trace =
      fun _menhir_stack _menhir_lexbuf _menhir_lexer ->
        let _menhir_s = MenhirState00 in
        let _tok = _menhir_lexer _menhir_lexbuf in
        match (_tok : MenhirBasics.token) with
        | Smv_trace_tokens.STATE ->
            _menhir_run_01 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s
        | Smv_trace_tokens.LOOP ->
            _menhir_run_09 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s
        | _ ->
            _eRR ()
    
  end
  
  let trace =
    fun _menhir_lexer _menhir_lexbuf ->
      let _menhir_stack = () in
      let MenhirBox_trace v = _menhir_run_00 _menhir_stack _menhir_lexbuf _menhir_lexer in
      v
  
end