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
    
    type token = Smv_trace_tokens.token
    
  end
  
  include MenhirBasics
  
  let _eRR =
    MenhirBasics.Error
  
  type _menhir_env = {
    _menhir_lexer: Lexing.lexbuf -> token;
    _menhir_lexbuf: Lexing.lexbuf;
    _menhir_token: token;
    mutable _menhir_error: bool
  }
  
  and _menhir_state = 
    | MenhirState13
    | MenhirState10
    | MenhirState7
    | MenhirState1
    | MenhirState0
  
# 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
    
       

# 101 "src/Smv_trace_parser.ml"
  
  let rec _menhir_goto_nonempty_list_state_ : _menhir_env -> 'ttv_tail -> _menhir_state -> (Outcome.state list) -> 'ttv_return =
    fun _menhir_env _menhir_stack _menhir_s _v ->
      let _menhir_stack = (_menhir_stack, _menhir_s, _v) in
      match _menhir_s with
      | MenhirState13 ->
          let _menhir_stack = Obj.magic _menhir_stack in
          let _menhir_stack = Obj.magic _menhir_stack in
          let ((_menhir_stack, _menhir_s, (x : (Outcome.state))), _, (xs : (Outcome.state list))) = _menhir_stack in
          let _v : (Outcome.state list) = 
# 223 "<standard.mly>"
    ( x :: xs )
# 114 "src/Smv_trace_parser.ml"
           in
          _menhir_goto_nonempty_list_state_ _menhir_env _menhir_stack _menhir_s _v
      | MenhirState0 ->
          let _menhir_stack = Obj.magic _menhir_stack in
          assert (not _menhir_env._menhir_error);
          let _tok = _menhir_env._menhir_token in
          (match _tok with
          | Smv_trace_tokens.EOF ->
              let _menhir_stack = Obj.magic _menhir_stack in
              let _menhir_stack = Obj.magic _menhir_stack in
              let (_menhir_stack, _menhir_s, (states : (Outcome.state list))) = _menhir_stack in
              let _2 = () in
              let _v : (
# 80 "src/Smv_trace_parser.mly"
       (Outcome.states)
# 130 "src/Smv_trace_parser.ml"
              ) = 
# 88 "src/Smv_trace_parser.mly"
    (
      remove_last states
    )
# 136 "src/Smv_trace_parser.ml"
               in
              let _menhir_stack = Obj.magic _menhir_stack in
              let _menhir_stack = Obj.magic _menhir_stack in
              let (_1 : (
# 80 "src/Smv_trace_parser.mly"
       (Outcome.states)
# 143 "src/Smv_trace_parser.ml"
              )) = _v in
              Obj.magic _1
          | _ ->
              assert (not _menhir_env._menhir_error);
              _menhir_env._menhir_error <- true;
              let _menhir_stack = Obj.magic _menhir_stack in
              let (_menhir_stack, _menhir_s, _) = _menhir_stack in
              _menhir_errorcase _menhir_env (Obj.magic _menhir_stack) _menhir_s)
      | _ ->
          _menhir_fail ()
  
  and _menhir_fail : unit -> 'a =
    fun () ->
      Printf.fprintf stderr "Internal failure -- please contact the parser generator's developers.\n%!";
      assert false
  
  and _menhir_goto_state : _menhir_env -> 'ttv_tail -> _menhir_state -> (Outcome.state) -> 'ttv_return =
    fun _menhir_env _menhir_stack _menhir_s _v ->
      let _menhir_stack = (_menhir_stack, _menhir_s, _v) in
      let _menhir_stack = Obj.magic _menhir_stack in
      assert (not _menhir_env._menhir_error);
      let _tok = _menhir_env._menhir_token in
      match _tok with
      | Smv_trace_tokens.LOOP ->
          _menhir_run9 _menhir_env (Obj.magic _menhir_stack) MenhirState13
      | Smv_trace_tokens.STATE ->
          _menhir_run1 _menhir_env (Obj.magic _menhir_stack) MenhirState13
      | Smv_trace_tokens.EOF ->
          let _menhir_stack = Obj.magic _menhir_stack in
          let (_menhir_stack, _menhir_s, (x : (Outcome.state))) = _menhir_stack in
          let _v : (Outcome.state list) = 
# 221 "<standard.mly>"
    ( [ x ] )
# 177 "src/Smv_trace_parser.ml"
           in
          _menhir_goto_nonempty_list_state_ _menhir_env _menhir_stack _menhir_s _v
      | _ ->
          assert (not _menhir_env._menhir_error);
          _menhir_env._menhir_error <- true;
          _menhir_errorcase _menhir_env (Obj.magic _menhir_stack) MenhirState13
  
  and _menhir_goto_list_atomic_ : _menhir_env -> 'ttv_tail -> _menhir_state -> ((Name.t * Tuple.t) option list) -> 'ttv_return =
    fun _menhir_env _menhir_stack _menhir_s _v ->
      match _menhir_s with
      | MenhirState1 ->
          let _menhir_stack = Obj.magic _menhir_stack in
          let _menhir_stack = Obj.magic _menhir_stack in
          let (ntl : ((Name.t * Tuple.t) option list)) = _v in
          let (_menhir_stack, _menhir_s) = _menhir_stack in
          let _2 = () in
          let _v : (Outcome.state) = let loop = 
# 115 "src/Smv_trace_parser.mly"
( false )
# 197 "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
    )
# 209 "src/Smv_trace_parser.ml"
           in
          _menhir_goto_state _menhir_env _menhir_stack _menhir_s _v
      | MenhirState7 ->
          let _menhir_stack = Obj.magic _menhir_stack in
          let _menhir_stack = Obj.magic _menhir_stack in
          let (xs : ((Name.t * Tuple.t) option list)) = _v in
          let (_menhir_stack, _menhir_s, (x : ((Name.t * Tuple.t) option))) = _menhir_stack in
          let _v : ((Name.t * Tuple.t) option list) = 
# 213 "<standard.mly>"
    ( x :: xs )
# 220 "src/Smv_trace_parser.ml"
           in
          _menhir_goto_list_atomic_ _menhir_env _menhir_stack _menhir_s _v
      | MenhirState10 ->
          let _menhir_stack = Obj.magic _menhir_stack in
          let _menhir_stack = Obj.magic _menhir_stack in
          let (ntl : ((Name.t * Tuple.t) option list)) = _v in
          let (_menhir_stack, _menhir_s) = _menhir_stack in
          let _2 = () in
          let _1 = () in
          let _v : (Outcome.state) = let loop = 
# 117 "src/Smv_trace_parser.mly"
    ( true )
# 233 "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
    )
# 245 "src/Smv_trace_parser.ml"
           in
          _menhir_goto_state _menhir_env _menhir_stack _menhir_s _v
      | _ ->
          _menhir_fail ()
  
  and _menhir_goto_atomic : _menhir_env -> 'ttv_tail -> _menhir_state -> ((Name.t * Tuple.t) option) -> 'ttv_return =
    fun _menhir_env _menhir_stack _menhir_s _v ->
      let _menhir_stack = (_menhir_stack, _menhir_s, _v) in
      let _menhir_stack = Obj.magic _menhir_stack in
      assert (not _menhir_env._menhir_error);
      let _tok = _menhir_env._menhir_token in
      match _tok with
      | Smv_trace_tokens.ATOMIC _v ->
          _menhir_run2 _menhir_env (Obj.magic _menhir_stack) MenhirState7 _v
      | Smv_trace_tokens.EOF | Smv_trace_tokens.LOOP | Smv_trace_tokens.STATE ->
          _menhir_reduce3 _menhir_env (Obj.magic _menhir_stack) MenhirState7
      | _ ->
          assert (not _menhir_env._menhir_error);
          _menhir_env._menhir_error <- true;
          _menhir_errorcase _menhir_env (Obj.magic _menhir_stack) MenhirState7
  
  and _menhir_reduce3 : _menhir_env -> 'ttv_tail -> _menhir_state -> 'ttv_return =
    fun _menhir_env _menhir_stack _menhir_s ->
      let _v : ((Name.t * Tuple.t) option list) = 
# 211 "<standard.mly>"
    ( [] )
# 272 "src/Smv_trace_parser.ml"
       in
      _menhir_goto_list_atomic_ _menhir_env _menhir_stack _menhir_s _v
  
  and _menhir_run2 : _menhir_env -> 'ttv_tail -> _menhir_state -> (
# 16 "src/Smv_trace_tokens.mly"
       (Name.t * Tuple.t)
# 279 "src/Smv_trace_parser.ml"
  ) -> 'ttv_return =
    fun _menhir_env _menhir_stack _menhir_s _v ->
      let _menhir_stack = (_menhir_stack, _menhir_s, _v) in
      let _menhir_env = _menhir_discard _menhir_env in
      let _tok = _menhir_env._menhir_token in
      match _tok with
      | Smv_trace_tokens.EQUAL ->
          let _menhir_stack = Obj.magic _menhir_stack in
          let _menhir_env = _menhir_discard _menhir_env in
          let _tok = _menhir_env._menhir_token in
          (match _tok with
          | Smv_trace_tokens.FALSE ->
              let _menhir_stack = Obj.magic _menhir_stack in
              let _menhir_env = _menhir_discard _menhir_env in
              let _menhir_stack = Obj.magic _menhir_stack in
              let (_menhir_stack, _menhir_s, (_1 : (
# 16 "src/Smv_trace_tokens.mly"
       (Name.t * Tuple.t)
# 298 "src/Smv_trace_parser.ml"
              ))) = _menhir_stack in
              let _3 = () in
              let _2 = () in
              let _v : ((Name.t * Tuple.t) option) = 
# 105 "src/Smv_trace_parser.mly"
    ( None )
# 305 "src/Smv_trace_parser.ml"
               in
              _menhir_goto_atomic _menhir_env _menhir_stack _menhir_s _v
          | Smv_trace_tokens.TRUE ->
              let _menhir_stack = Obj.magic _menhir_stack in
              let _menhir_env = _menhir_discard _menhir_env in
              let _menhir_stack = Obj.magic _menhir_stack in
              let (_menhir_stack, _menhir_s, (v : (
# 16 "src/Smv_trace_tokens.mly"
       (Name.t * Tuple.t)
# 315 "src/Smv_trace_parser.ml"
              ))) = _menhir_stack in
              let _3 = () in
              let _2 = () in
              let _v : ((Name.t * Tuple.t) option) = 
# 107 "src/Smv_trace_parser.mly"
    ( Some v )
# 322 "src/Smv_trace_parser.ml"
               in
              _menhir_goto_atomic _menhir_env _menhir_stack _menhir_s _v
          | _ ->
              assert (not _menhir_env._menhir_error);
              _menhir_env._menhir_error <- true;
              let _menhir_stack = Obj.magic _menhir_stack in
              let (_menhir_stack, _menhir_s, _) = _menhir_stack in
              _menhir_errorcase _menhir_env (Obj.magic _menhir_stack) _menhir_s)
      | _ ->
          assert (not _menhir_env._menhir_error);
          _menhir_env._menhir_error <- true;
          let _menhir_stack = Obj.magic _menhir_stack in
          let (_menhir_stack, _menhir_s, _) = _menhir_stack in
          _menhir_errorcase _menhir_env (Obj.magic _menhir_stack) _menhir_s
  
  and _menhir_errorcase : _menhir_env -> 'ttv_tail -> _menhir_state -> 'ttv_return =
    fun _menhir_env _menhir_stack _menhir_s ->
      match _menhir_s with
      | MenhirState13 ->
          let _menhir_stack = Obj.magic _menhir_stack in
          let (_menhir_stack, _menhir_s, _) = _menhir_stack in
          _menhir_errorcase _menhir_env (Obj.magic _menhir_stack) _menhir_s
      | MenhirState10 ->
          let _menhir_stack = Obj.magic _menhir_stack in
          let (_menhir_stack, _menhir_s) = _menhir_stack in
          _menhir_errorcase _menhir_env (Obj.magic _menhir_stack) _menhir_s
      | MenhirState7 ->
          let _menhir_stack = Obj.magic _menhir_stack in
          let (_menhir_stack, _menhir_s, _) = _menhir_stack in
          _menhir_errorcase _menhir_env (Obj.magic _menhir_stack) _menhir_s
      | MenhirState1 ->
          let _menhir_stack = Obj.magic _menhir_stack in
          let (_menhir_stack, _menhir_s) = _menhir_stack in
          _menhir_errorcase _menhir_env (Obj.magic _menhir_stack) _menhir_s
      | MenhirState0 ->
          let _menhir_stack = Obj.magic _menhir_stack in
          raise _eRR
  
  and _menhir_run1 : _menhir_env -> 'ttv_tail -> _menhir_state -> 'ttv_return =
    fun _menhir_env _menhir_stack _menhir_s ->
      let _menhir_stack = (_menhir_stack, _menhir_s) in
      let _menhir_env = _menhir_discard _menhir_env in
      let _tok = _menhir_env._menhir_token in
      match _tok with
      | Smv_trace_tokens.ATOMIC _v ->
          _menhir_run2 _menhir_env (Obj.magic _menhir_stack) MenhirState1 _v
      | Smv_trace_tokens.EOF | Smv_trace_tokens.LOOP | Smv_trace_tokens.STATE ->
          _menhir_reduce3 _menhir_env (Obj.magic _menhir_stack) MenhirState1
      | _ ->
          assert (not _menhir_env._menhir_error);
          _menhir_env._menhir_error <- true;
          _menhir_errorcase _menhir_env (Obj.magic _menhir_stack) MenhirState1
  
  and _menhir_run9 : _menhir_env -> 'ttv_tail -> _menhir_state -> 'ttv_return =
    fun _menhir_env _menhir_stack _menhir_s ->
      let _menhir_stack = (_menhir_stack, _menhir_s) in
      let _menhir_env = _menhir_discard _menhir_env in
      let _tok = _menhir_env._menhir_token in
      match _tok with
      | Smv_trace_tokens.STATE ->
          let _menhir_stack = Obj.magic _menhir_stack in
          let _menhir_env = _menhir_discard _menhir_env in
          let _tok = _menhir_env._menhir_token in
          (match _tok with
          | Smv_trace_tokens.ATOMIC _v ->
              _menhir_run2 _menhir_env (Obj.magic _menhir_stack) MenhirState10 _v
          | Smv_trace_tokens.EOF | Smv_trace_tokens.LOOP | Smv_trace_tokens.STATE ->
              _menhir_reduce3 _menhir_env (Obj.magic _menhir_stack) MenhirState10
          | _ ->
              assert (not _menhir_env._menhir_error);
              _menhir_env._menhir_error <- true;
              _menhir_errorcase _menhir_env (Obj.magic _menhir_stack) MenhirState10)
      | _ ->
          assert (not _menhir_env._menhir_error);
          _menhir_env._menhir_error <- true;
          let _menhir_stack = Obj.magic _menhir_stack in
          let (_menhir_stack, _menhir_s) = _menhir_stack in
          _menhir_errorcase _menhir_env (Obj.magic _menhir_stack) _menhir_s
  
  and _menhir_discard : _menhir_env -> _menhir_env =
    fun _menhir_env ->
      let lexer = _menhir_env._menhir_lexer in
      let lexbuf = _menhir_env._menhir_lexbuf in
      let _tok = lexer lexbuf in
      {
        _menhir_lexer = lexer;
        _menhir_lexbuf = lexbuf;
        _menhir_token = _tok;
        _menhir_error = false;
      }
  
  and trace : (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (
# 80 "src/Smv_trace_parser.mly"
       (Outcome.states)
# 417 "src/Smv_trace_parser.ml"
  ) =
    fun lexer lexbuf ->
      let _menhir_env = let _tok = Obj.magic () in
      {
        _menhir_lexer = lexer;
        _menhir_lexbuf = lexbuf;
        _menhir_token = _tok;
        _menhir_error = false;
      } in
      Obj.magic (let _menhir_stack = ((), _menhir_env._menhir_lexbuf.Lexing.lex_curr_p) in
      let _menhir_env = _menhir_discard _menhir_env in
      let _tok = _menhir_env._menhir_token in
      match _tok with
      | Smv_trace_tokens.LOOP ->
          _menhir_run9 _menhir_env (Obj.magic _menhir_stack) MenhirState0
      | Smv_trace_tokens.STATE ->
          _menhir_run1 _menhir_env (Obj.magic _menhir_stack) MenhirState0
      | _ ->
          assert (not _menhir_env._menhir_error);
          _menhir_env._menhir_error <- true;
          _menhir_errorcase _menhir_env (Obj.magic _menhir_stack) MenhirState0)
  
# 269 "<standard.mly>"
  

# 443 "src/Smv_trace_parser.ml"
  
end