nusmv - 当我使用 nusmv 检查 LTL 规范时，我遇到了一些语法错误问题。错误信息是：at token "LTLSPEC": syntax error

Question

TRANS
case
(AMF_NAS_T6 | AMF_NAS_T17 | AMF_NAS_T21 | AMF_NAS_T22 | AMF_NAS_T45 | AMF_NAS_T49 | AMF_NAS_T50 | AMF_NAS_T65 | AMF_NAS_T70 )   :   next(amf_seq)   =   ((amf_seq + 1) mod 32)  ;
TRUE    :   next(amf_seq)   =   amf_seq ;

LTLSPEC
    F (enable_N1 & X G (!enable_N1)) &  
      (power_on & X (G !power_on)) &
    G(  !reg_failure
        & !power_off
        & !ue_inactivity_detected
        & !smcmd_mac_failure
        & ! ta_changed
        & !uederegrequested
        & sec_cap_match
        & inj_adv_act_AU != adv_AU_auth_reject
        & inj_adv_act_AU != adv_AU_reg_reject
        & inj_adv_act_AU != adv_AU_nwk_dereg_req
        & inj_adv_act_AU != adv_AU_service_reject
        & inj_adv_act_AU != adv_AU_service_accept
        & inj_adv_act_AU != adv_AU_config_update_cmd
        & inj_adv_act_AU != adv_AU_auth_req
        & inj_adv_act_AU != adv_AU_id_req
        & inj_adv_act_AU != adv_AU_nwk_dereg_accept
        & inj_adv_act_AU != adv_AU_reg_accept
        & inj_adv_act_AU != adv_AU_ue_ctx_release
    )
    ->
        -- G((ue_nas_state = ue_registered
        -- & ueregcompleted
        -- & ue_nas_action = sm_complete) -> O (chan_AU = chanAU_sm_command &  amf_nas_action = sm_command)) ;
        G (((ue_nas_state = ue_registered & ueregcompleted) & ue_nas_action = sm_complete) 
            -> O (chan_AU = chanAU_sm_command & amf_nas_action = sm_command));