[
    {
        "reqid": "DRC_S004_SCRAM_STAY",
        "parent_reqid": "",
        "project": "PWR_HYBRID_3",
        "rationale": "",
        "comments": "",
        "fulltext": "Whenever control_mode = q_scram & !manual_reset   DRC shall at the next timepoint satisfy control_mode = q_scram",
        "semantics": {
            "type": "nasa",
            "scope": {
                "type": "null"
            },
            "condition": "holding",
            "probability": "null",
            "timing": "next",
            "response": "satisfaction",
            "variables": [
                "control_mode",
                "q_scram",
                "manual_reset"
            ],
            "qualifier_word": "whenever",
            "pre_condition": "(control_mode = q_scram & ! manual_reset)",
            "regular_condition": "(control_mode = q_scram & ! manual_reset)",
            "conditionTextRange": [
                0,
                46
            ],
            "component_name": "DRC",
            "componentTextRange": [
                50,
                52
            ],
            "timingTextRange": [
                60,
                80
            ],
            "post_condition": "(control_mode = q_scram)",
            "responseTextRange": [
                82,
                111
            ],
            "diagramVariables": "CC = <b><i>(control_mode = q_scram & ! manual_reset)</i></b>, Response = <b><i>(control_mode = q_scram)</i></b>.",
            "description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: every point in the interval where <b><i>(control_mode = q_scram & ! manual_reset)</i></b> is true.<br>REQUIRED BEHAVIOR: for every trigger, <b><i>(control_mode = q_scram)</i></b> must hold at the next time step.",
            "probabilistic_description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: every point in the interval where <b><i>(control_mode = q_scram & ! manual_reset)</i></b> is true.<br>REQUIRED BEHAVIOR: for every trigger, with probability >=1, <b><i>(control_mode = q_scram)</i></b> must hold at the next time step.",
            "diagram": "_media/user-interface/examples/svgDiagrams/null_holding_next_satisfaction.svg",
            "scope_mode_pt": "BAD_PT",
            "scope_mode_ft": "BAD_FT",
            "regular_condition_unexp_pt": "((control_mode = q_scram) & (! manual_reset))",
            "regular_condition_unexp_ft": "((control_mode = q_scram) & (! manual_reset))",
            "regular_condition_unexp_pctl": "((control_mode = q_scram) & (! manual_reset))",
            "regular_condition_SMV_pt": "((control_mode = q_scram) & (! manual_reset))",
            "regular_condition_SMV_ft": "((control_mode = q_scram) & (! manual_reset))",
            "regular_condition_MLTL_ft": "((control_mode = q_scram) & (! manual_reset))",
            "regular_condition_PRISM_pctl": "((control_mode = q_scram) & (! manual_reset))",
            "post_condition_unexp_pt": "(control_mode = q_scram)",
            "post_condition_unexp_ft": "(control_mode = q_scram)",
            "post_condition_unexp_pctl": "(control_mode = q_scram)",
            "post_condition_SMV_pt": "(control_mode = q_scram)",
            "post_condition_SMV_ft": "(control_mode = q_scram)",
            "post_condition_MLTL_ft": "(control_mode = q_scram)",
            "post_condition_PRISM_pctl": "(control_mode = q_scram)",
            "ft": "(LAST V (((control_mode = q_scram) & (! manual_reset)) -> (LAST | (X (control_mode = q_scram)))))",
            "pt": "(H ((Y ((control_mode = q_scram) & (! manual_reset))) -> ((control_mode = q_scram) | (Z FALSE))))",
            "pctl": "P>=1[(G (((control_mode = q_scram) & (! manual_reset)) => (P>=1[(LAST | (X (control_mode = q_scram)))])))]",
            "ptExpanded": "(H ((Y ((control_mode = q_scram) & (! manual_reset))) -> ((control_mode = q_scram) | (Z FALSE))))",
            "CoCoSpecCode": "H((YtoPre(((control_mode = q_scram) and not (manual_reset))) => ((control_mode = q_scram) or ZtoPre(false))))",
            "ftExpanded": "(LAST V (((control_mode = q_scram) & (! manual_reset)) -> (LAST | (X (control_mode = q_scram)))))",
            "pctlExpanded": "P>=1[(G (((control_mode = q_scram) & (! manual_reset)) => (P>=1[(false | (X (control_mode = q_scram)))])))]",
            "ftInfAUExpanded": "(G (((control_mode = q_scram) & (! manual_reset)) -> (X (control_mode = q_scram))))",
            "mltlExpanded": "(G[0,M] (p0 -> (F[1,1] p1)))",
            "WESTMapping": "p0: ((control_mode = q_scram) & (! manual_reset))<br/>p1: (control_mode = q_scram)",
            "R2U2Code": "(((control_mode == q_scram) && (! manual_reset)) -> (F[1,1] (control_mode == q_scram)))",
            "component": "DRC"
        },
        "status": "",
        "_id": "68403100-3463-11f1-b848-f314240f620d"
    },
    {
        "reqid": "DRC_T001_SHUTDOWN_TO_HEATUP",
        "parent_reqid": "",
        "project": "PWR_HYBRID_3",
        "rationale": "",
        "comments": "",
        "fulltext": "Upon control_mode = q_shutdown & t_avg_above_min   DRC shall at the next timepoint satisfy control_mode = q_heatup",
        "semantics": {
            "type": "nasa",
            "scope": {
                "type": "null"
            },
            "condition": "regular",
            "probability": "null",
            "timing": "next",
            "response": "satisfaction",
            "variables": [
                "control_mode",
                "q_shutdown",
                "t_avg_above_min",
                "q_heatup"
            ],
            "qualifier_word": "upon",
            "pre_condition": "(control_mode = q_shutdown & t_avg_above_min)",
            "regular_condition": "(control_mode = q_shutdown & t_avg_above_min)",
            "conditionTextRange": [
                0,
                47
            ],
            "component_name": "DRC",
            "componentTextRange": [
                51,
                53
            ],
            "timingTextRange": [
                61,
                81
            ],
            "post_condition": "(control_mode = q_heatup)",
            "responseTextRange": [
                83,
                113
            ],
            "diagramVariables": "TC = <b><i>(control_mode = q_shutdown & t_avg_above_min)</i></b>, Response = <b><i>(control_mode = q_heatup)</i></b>.",
            "description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: first point in the interval if <b><i>(control_mode = q_shutdown & t_avg_above_min)</i></b> is true and any point in the interval where <b><i>(control_mode = q_shutdown & t_avg_above_min)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, <b><i>(control_mode = q_heatup)</i></b> must hold at the next time step.",
            "probabilistic_description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: first point in the interval if <b><i>(control_mode = q_shutdown & t_avg_above_min)</i></b> is true and any point in the interval where <b><i>(control_mode = q_shutdown & t_avg_above_min)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, with probability >=1, <b><i>(control_mode = q_heatup)</i></b> must hold at the next time step.",
            "diagram": "_media/user-interface/examples/svgDiagrams/null_regular_next_satisfaction.svg",
            "scope_mode_pt": "BAD_PT",
            "scope_mode_ft": "BAD_FT",
            "regular_condition_unexp_pt": "((control_mode = q_shutdown) & t_avg_above_min)",
            "regular_condition_unexp_ft": "((control_mode = q_shutdown) & t_avg_above_min)",
            "regular_condition_unexp_pctl": "((control_mode = q_shutdown) & t_avg_above_min)",
            "regular_condition_SMV_pt": "((control_mode = q_shutdown) & t_avg_above_min)",
            "regular_condition_SMV_ft": "((control_mode = q_shutdown) & t_avg_above_min)",
            "regular_condition_MLTL_ft": "((control_mode = q_shutdown) & t_avg_above_min)",
            "regular_condition_PRISM_pctl": "((control_mode = q_shutdown) & t_avg_above_min)",
            "post_condition_unexp_pt": "(control_mode = q_heatup)",
            "post_condition_unexp_ft": "(control_mode = q_heatup)",
            "post_condition_unexp_pctl": "(control_mode = q_heatup)",
            "post_condition_SMV_pt": "(control_mode = q_heatup)",
            "post_condition_SMV_ft": "(control_mode = q_heatup)",
            "post_condition_MLTL_ft": "(control_mode = q_heatup)",
            "post_condition_PRISM_pctl": "(control_mode = q_heatup)",
            "ft": "((LAST V (((! ((control_mode = q_shutdown) & t_avg_above_min)) & ((! LAST) & (X ((control_mode = q_shutdown) & t_avg_above_min)))) -> (X (LAST | (X (control_mode = q_heatup)))))) & (((control_mode = q_shutdown) & t_avg_above_min) -> (LAST | (X (control_mode = q_heatup)))))",
            "pt": "(H ((Y (((control_mode = q_shutdown) & t_avg_above_min) & (Z (! ((control_mode = q_shutdown) & t_avg_above_min))))) -> ((control_mode = q_heatup) | (Z FALSE))))",
            "pctl": "P>=1[((G (((! ((control_mode = q_shutdown) & t_avg_above_min)) & (X ((control_mode = q_shutdown) & t_avg_above_min))) => (X (P>=1[(LAST | (X (control_mode = q_heatup)))])))) & (((control_mode = q_shutdown) & t_avg_above_min) => (P>=1[(LAST | (X (control_mode = q_heatup)))])))]",
            "ptExpanded": "(H ((Y (((control_mode = q_shutdown) & t_avg_above_min) & (Z (! ((control_mode = q_shutdown) & t_avg_above_min))))) -> ((control_mode = q_heatup) | (Z FALSE))))",
            "CoCoSpecCode": "H((YtoPre((((control_mode = q_shutdown) and t_avg_above_min) and ZtoPre(not (((control_mode = q_shutdown) and t_avg_above_min))))) => ((control_mode = q_heatup) or ZtoPre(false))))",
            "ftExpanded": "((LAST V (((! ((control_mode = q_shutdown) & t_avg_above_min)) & ((! LAST) & (X ((control_mode = q_shutdown) & t_avg_above_min)))) -> (X (LAST | (X (control_mode = q_heatup)))))) & (((control_mode = q_shutdown) & t_avg_above_min) -> (LAST | (X (control_mode = q_heatup)))))",
            "pctlExpanded": "P>=1[((G (((! ((control_mode = q_shutdown) & t_avg_above_min)) & (X ((control_mode = q_shutdown) & t_avg_above_min))) => (X (P>=1[(false | (X (control_mode = q_heatup)))])))) & (((control_mode = q_shutdown) & t_avg_above_min) => (P>=1[(false | (X (control_mode = q_heatup)))])))]",
            "ftInfAUExpanded": "((G (((! ((control_mode = q_shutdown) & t_avg_above_min)) & (X ((control_mode = q_shutdown) & t_avg_above_min))) -> (X (X (control_mode = q_heatup))))) & (((control_mode = q_shutdown) & t_avg_above_min) -> (X (control_mode = q_heatup))))",
            "mltlExpanded": "((G[0,M] (((! p0) & (F[1,1] p0)) -> (F[2,2] p1))) & (p0 -> (F[1,1] p1)))",
            "WESTMapping": "p0: ((control_mode = q_shutdown) & t_avg_above_min)<br/>p1: (control_mode = q_heatup)",
            "R2U2Code": "((((! ((control_mode == q_shutdown) && t_avg_above_min)) && (F[1,1] ((control_mode == q_shutdown) && t_avg_above_min))) -> (F[2,2] (control_mode == q_heatup))) && (((TAU == 0) && ((control_mode == q_shutdown) && t_avg_above_min)) -> (F[1,1] (control_mode == q_heatup))))",
            "component": "DRC"
        },
        "status": "",
        "_id": "68403101-3463-11f1-b848-f314240f620d"
    },
    {
        "reqid": "DRC_T002_HEATUP_TO_OPERATION",
        "parent_reqid": "",
        "project": "PWR_HYBRID_3",
        "rationale": "",
        "comments": "",
        "fulltext": "Upon control_mode = q_heatup & t_avg_in_range & p_above_crit & inv1_holds  DRC shall at the next timepoint satisfy control_mode = q_operation",
        "semantics": {
            "type": "nasa",
            "scope": {
                "type": "null"
            },
            "condition": "regular",
            "probability": "null",
            "timing": "next",
            "response": "satisfaction",
            "variables": [
                "control_mode",
                "q_heatup",
                "t_avg_in_range",
                "p_above_crit",
                "inv1_holds",
                "q_operation"
            ],
            "qualifier_word": "upon",
            "pre_condition": "(control_mode = q_heatup & t_avg_in_range & p_above_crit & inv1_holds)",
            "regular_condition": "(control_mode = q_heatup & t_avg_in_range & p_above_crit & inv1_holds)",
            "conditionTextRange": [
                0,
                72
            ],
            "component_name": "DRC",
            "componentTextRange": [
                75,
                77
            ],
            "timingTextRange": [
                85,
                105
            ],
            "post_condition": "(control_mode = q_operation)",
            "responseTextRange": [
                107,
                140
            ],
            "diagramVariables": "TC = <b><i>(control_mode = q_heatup & t_avg_in_range & p_above_crit & inv1_holds)</i></b>, Response = <b><i>(control_mode = q_operation)</i></b>.",
            "description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: first point in the interval if <b><i>(control_mode = q_heatup & t_avg_in_range & p_above_crit & inv1_holds)</i></b> is true and any point in the interval where <b><i>(control_mode = q_heatup & t_avg_in_range & p_above_crit & inv1_holds)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, <b><i>(control_mode = q_operation)</i></b> must hold at the next time step.",
            "probabilistic_description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: first point in the interval if <b><i>(control_mode = q_heatup & t_avg_in_range & p_above_crit & inv1_holds)</i></b> is true and any point in the interval where <b><i>(control_mode = q_heatup & t_avg_in_range & p_above_crit & inv1_holds)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, with probability >=1, <b><i>(control_mode = q_operation)</i></b> must hold at the next time step.",
            "diagram": "_media/user-interface/examples/svgDiagrams/null_regular_next_satisfaction.svg",
            "scope_mode_pt": "BAD_PT",
            "scope_mode_ft": "BAD_FT",
            "regular_condition_unexp_pt": "((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds)",
            "regular_condition_unexp_ft": "((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds)",
            "regular_condition_unexp_pctl": "((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds)",
            "regular_condition_SMV_pt": "((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds)",
            "regular_condition_SMV_ft": "((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds)",
            "regular_condition_MLTL_ft": "((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds)",
            "regular_condition_PRISM_pctl": "((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds)",
            "post_condition_unexp_pt": "(control_mode = q_operation)",
            "post_condition_unexp_ft": "(control_mode = q_operation)",
            "post_condition_unexp_pctl": "(control_mode = q_operation)",
            "post_condition_SMV_pt": "(control_mode = q_operation)",
            "post_condition_SMV_ft": "(control_mode = q_operation)",
            "post_condition_MLTL_ft": "(control_mode = q_operation)",
            "post_condition_PRISM_pctl": "(control_mode = q_operation)",
            "ft": "((LAST V (((! ((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds)) & ((! LAST) & (X ((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds)))) -> (X (LAST | (X (control_mode = q_operation)))))) & (((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds) -> (LAST | (X (control_mode = q_operation)))))",
            "pt": "(H ((Y (((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds) & (Z (! ((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds))))) -> ((control_mode = q_operation) | (Z FALSE))))",
            "pctl": "P>=1[((G (((! ((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds)) & (X ((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds))) => (X (P>=1[(LAST | (X (control_mode = q_operation)))])))) & (((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds) => (P>=1[(LAST | (X (control_mode = q_operation)))])))]",
            "ptExpanded": "(H ((Y (((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds) & (Z (! ((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds))))) -> ((control_mode = q_operation) | (Z FALSE))))",
            "CoCoSpecCode": "H((YtoPre((((((control_mode = q_heatup) and t_avg_in_range) and p_above_crit) and inv1_holds) and ZtoPre(not (((((control_mode = q_heatup) and t_avg_in_range) and p_above_crit) and inv1_holds))))) => ((control_mode = q_operation) or ZtoPre(false))))",
            "ftExpanded": "((LAST V (((! ((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds)) & ((! LAST) & (X ((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds)))) -> (X (LAST | (X (control_mode = q_operation)))))) & (((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds) -> (LAST | (X (control_mode = q_operation)))))",
            "pctlExpanded": "P>=1[((G (((! ((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds)) & (X ((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds))) => (X (P>=1[(false | (X (control_mode = q_operation)))])))) & (((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds) => (P>=1[(false | (X (control_mode = q_operation)))])))]",
            "ftInfAUExpanded": "((G (((! ((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds)) & (X ((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds))) -> (X (X (control_mode = q_operation))))) & (((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds) -> (X (control_mode = q_operation))))",
            "mltlExpanded": "((G[0,M] (((! p0) & (F[1,1] p0)) -> (F[2,2] p1))) & (p0 -> (F[1,1] p1)))",
            "WESTMapping": "p0: ((((control_mode = q_heatup) & t_avg_in_range) & p_above_crit) & inv1_holds)<br/>p1: (control_mode = q_operation)",
            "R2U2Code": "((((! ((((control_mode == q_heatup) && t_avg_in_range) && p_above_crit) && inv1_holds)) && (F[1,1] ((((control_mode == q_heatup) && t_avg_in_range) && p_above_crit) && inv1_holds))) -> (F[2,2] (control_mode == q_operation))) && (((TAU == 0) && ((((control_mode == q_heatup) && t_avg_in_range) && p_above_crit) && inv1_holds)) -> (F[1,1] (control_mode == q_operation))))",
            "component": "DRC"
        },
        "status": "",
        "_id": "68403102-3463-11f1-b848-f314240f620d"
    },
    {
        "reqid": "DRC_A001_MODE_VALID",
        "parent_reqid": "",
        "project": "PWR_HYBRID_3",
        "rationale": "",
        "comments": "",
        "fulltext": "DRC shall always satisfy control_mode = q_shutdown | control_mode = q_heatup | control_mode = q_operation | control_mode = q_scram",
        "semantics": {
            "type": "nasa",
            "scope": {
                "type": "null"
            },
            "condition": "null",
            "probability": "null",
            "timing": "always",
            "response": "satisfaction",
            "variables": [
                "control_mode",
                "q_shutdown",
                "q_heatup",
                "q_operation",
                "q_scram"
            ],
            "component_name": "DRC",
            "componentTextRange": [
                0,
                2
            ],
            "timingTextRange": [
                10,
                15
            ],
            "post_condition": "(control_mode = q_shutdown | control_mode = q_heatup | control_mode = q_operation | control_mode = q_scram)",
            "responseTextRange": [
                17,
                129
            ],
            "diagramVariables": "Response = <b><i>(control_mode = q_shutdown | control_mode = q_heatup | control_mode = q_operation | control_mode = q_scram)</i></b>.",
            "description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: first point in the interval.<br>REQUIRED BEHAVIOR: for every trigger, <b><i>(control_mode = q_shutdown | control_mode = q_heatup | control_mode = q_operation | control_mode = q_scram)</i></b> must hold at all time points between (and including) the trigger and the end of the interval.",
            "probabilistic_description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: first point in the interval.<br>REQUIRED BEHAVIOR: for every trigger, with probability >=1, <b><i>(control_mode = q_shutdown | control_mode = q_heatup | control_mode = q_operation | control_mode = q_scram)</i></b> must hold at all time points between (and including) the trigger and the end of the interval.",
            "diagram": "_media/user-interface/examples/svgDiagrams/null_null_always_satisfaction.svg",
            "scope_mode_pt": "BAD_PT",
            "scope_mode_ft": "BAD_FT",
            "post_condition_unexp_pt": "((((control_mode = q_shutdown) | (control_mode = q_heatup)) | (control_mode = q_operation)) | (control_mode = q_scram))",
            "post_condition_unexp_ft": "((((control_mode = q_shutdown) | (control_mode = q_heatup)) | (control_mode = q_operation)) | (control_mode = q_scram))",
            "post_condition_unexp_pctl": "((((control_mode = q_shutdown) | (control_mode = q_heatup)) | (control_mode = q_operation)) | (control_mode = q_scram))",
            "post_condition_SMV_pt": "((((control_mode = q_shutdown) | (control_mode = q_heatup)) | (control_mode = q_operation)) | (control_mode = q_scram))",
            "post_condition_SMV_ft": "((((control_mode = q_shutdown) | (control_mode = q_heatup)) | (control_mode = q_operation)) | (control_mode = q_scram))",
            "post_condition_MLTL_ft": "((((control_mode = q_shutdown) | (control_mode = q_heatup)) | (control_mode = q_operation)) | (control_mode = q_scram))",
            "post_condition_PRISM_pctl": "((((control_mode = q_shutdown) | (control_mode = q_heatup)) | (control_mode = q_operation)) | (control_mode = q_scram))",
            "ft": "(LAST V ((((control_mode = q_shutdown) | (control_mode = q_heatup)) | (control_mode = q_operation)) | (control_mode = q_scram)))",
            "pt": "(H ((((control_mode = q_shutdown) | (control_mode = q_heatup)) | (control_mode = q_operation)) | (control_mode = q_scram)))",
            "pctl": "(P>=1[(G ((((control_mode = q_shutdown) | (control_mode = q_heatup)) | (control_mode = q_operation)) | (control_mode = q_scram)))])",
            "ptExpanded": "(H ((((control_mode = q_shutdown) | (control_mode = q_heatup)) | (control_mode = q_operation)) | (control_mode = q_scram)))",
            "CoCoSpecCode": "H(((((control_mode = q_shutdown) or (control_mode = q_heatup)) or (control_mode = q_operation)) or (control_mode = q_scram)))",
            "ftExpanded": "(LAST V ((((control_mode = q_shutdown) | (control_mode = q_heatup)) | (control_mode = q_operation)) | (control_mode = q_scram)))",
            "pctlExpanded": "(P>=1[(G ((((control_mode = q_shutdown) | (control_mode = q_heatup)) | (control_mode = q_operation)) | (control_mode = q_scram)))])",
            "ftInfAUExpanded": "(G ((((control_mode = q_shutdown) | (control_mode = q_heatup)) | (control_mode = q_operation)) | (control_mode = q_scram)))",
            "mltlExpanded": "(G[0,M] p0)",
            "WESTMapping": "p0: ((((control_mode = q_shutdown) | (control_mode = q_heatup)) | (control_mode = q_operation)) | (control_mode = q_scram))",
            "R2U2Code": "((((control_mode == q_shutdown) || (control_mode == q_heatup)) || (control_mode == q_operation)) || (control_mode == q_scram))",
            "component": "DRC"
        },
        "status": "",
        "_id": "68403103-3463-11f1-b848-f314240f620d"
    },
    {
        "reqid": "DRC_T003_HEATUP_TO_SCRAM",
        "parent_reqid": "",
        "project": "PWR_HYBRID_3",
        "rationale": "",
        "comments": "",
        "fulltext": "Upon control_mode = q_heatup & !inv1_holds   DRC shall at the next timepoint satisfy control_mode = q_scram",
        "semantics": {
            "type": "nasa",
            "scope": {
                "type": "null"
            },
            "condition": "regular",
            "probability": "null",
            "timing": "next",
            "response": "satisfaction",
            "variables": [
                "control_mode",
                "q_heatup",
                "inv1_holds",
                "q_scram"
            ],
            "qualifier_word": "upon",
            "pre_condition": "(control_mode = q_heatup & ! inv1_holds)",
            "regular_condition": "(control_mode = q_heatup & ! inv1_holds)",
            "conditionTextRange": [
                0,
                41
            ],
            "component_name": "DRC",
            "componentTextRange": [
                45,
                47
            ],
            "timingTextRange": [
                55,
                75
            ],
            "post_condition": "(control_mode = q_scram)",
            "responseTextRange": [
                77,
                106
            ],
            "diagramVariables": "TC = <b><i>(control_mode = q_heatup & ! inv1_holds)</i></b>, Response = <b><i>(control_mode = q_scram)</i></b>.",
            "description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: first point in the interval if <b><i>(control_mode = q_heatup & ! inv1_holds)</i></b> is true and any point in the interval where <b><i>(control_mode = q_heatup & ! inv1_holds)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, <b><i>(control_mode = q_scram)</i></b> must hold at the next time step.",
            "probabilistic_description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: first point in the interval if <b><i>(control_mode = q_heatup & ! inv1_holds)</i></b> is true and any point in the interval where <b><i>(control_mode = q_heatup & ! inv1_holds)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, with probability >=1, <b><i>(control_mode = q_scram)</i></b> must hold at the next time step.",
            "diagram": "_media/user-interface/examples/svgDiagrams/null_regular_next_satisfaction.svg",
            "scope_mode_pt": "BAD_PT",
            "scope_mode_ft": "BAD_FT",
            "regular_condition_unexp_pt": "((control_mode = q_heatup) & (! inv1_holds))",
            "regular_condition_unexp_ft": "((control_mode = q_heatup) & (! inv1_holds))",
            "regular_condition_unexp_pctl": "((control_mode = q_heatup) & (! inv1_holds))",
            "regular_condition_SMV_pt": "((control_mode = q_heatup) & (! inv1_holds))",
            "regular_condition_SMV_ft": "((control_mode = q_heatup) & (! inv1_holds))",
            "regular_condition_MLTL_ft": "((control_mode = q_heatup) & (! inv1_holds))",
            "regular_condition_PRISM_pctl": "((control_mode = q_heatup) & (! inv1_holds))",
            "post_condition_unexp_pt": "(control_mode = q_scram)",
            "post_condition_unexp_ft": "(control_mode = q_scram)",
            "post_condition_unexp_pctl": "(control_mode = q_scram)",
            "post_condition_SMV_pt": "(control_mode = q_scram)",
            "post_condition_SMV_ft": "(control_mode = q_scram)",
            "post_condition_MLTL_ft": "(control_mode = q_scram)",
            "post_condition_PRISM_pctl": "(control_mode = q_scram)",
            "ft": "((LAST V (((! ((control_mode = q_heatup) & (! inv1_holds))) & ((! LAST) & (X ((control_mode = q_heatup) & (! inv1_holds))))) -> (X (LAST | (X (control_mode = q_scram)))))) & (((control_mode = q_heatup) & (! inv1_holds)) -> (LAST | (X (control_mode = q_scram)))))",
            "pt": "(H ((Y (((control_mode = q_heatup) & (! inv1_holds)) & (Z (! ((control_mode = q_heatup) & (! inv1_holds)))))) -> ((control_mode = q_scram) | (Z FALSE))))",
            "pctl": "P>=1[((G (((! ((control_mode = q_heatup) & (! inv1_holds))) & (X ((control_mode = q_heatup) & (! inv1_holds)))) => (X (P>=1[(LAST | (X (control_mode = q_scram)))])))) & (((control_mode = q_heatup) & (! inv1_holds)) => (P>=1[(LAST | (X (control_mode = q_scram)))])))]",
            "ptExpanded": "(H ((Y (((control_mode = q_heatup) & (! inv1_holds)) & (Z (! ((control_mode = q_heatup) & (! inv1_holds)))))) -> ((control_mode = q_scram) | (Z FALSE))))",
            "CoCoSpecCode": "H((YtoPre((((control_mode = q_heatup) and not (inv1_holds)) and ZtoPre(not (((control_mode = q_heatup) and not (inv1_holds)))))) => ((control_mode = q_scram) or ZtoPre(false))))",
            "ftExpanded": "((LAST V (((! ((control_mode = q_heatup) & (! inv1_holds))) & ((! LAST) & (X ((control_mode = q_heatup) & (! inv1_holds))))) -> (X (LAST | (X (control_mode = q_scram)))))) & (((control_mode = q_heatup) & (! inv1_holds)) -> (LAST | (X (control_mode = q_scram)))))",
            "pctlExpanded": "P>=1[((G (((! ((control_mode = q_heatup) & (! inv1_holds))) & (X ((control_mode = q_heatup) & (! inv1_holds)))) => (X (P>=1[(false | (X (control_mode = q_scram)))])))) & (((control_mode = q_heatup) & (! inv1_holds)) => (P>=1[(false | (X (control_mode = q_scram)))])))]",
            "ftInfAUExpanded": "((G (((! ((control_mode = q_heatup) & (! inv1_holds))) & (X ((control_mode = q_heatup) & (! inv1_holds)))) -> (X (X (control_mode = q_scram))))) & (((control_mode = q_heatup) & (! inv1_holds)) -> (X (control_mode = q_scram))))",
            "mltlExpanded": "((G[0,M] (((! p0) & (F[1,1] p0)) -> (F[2,2] p1))) & (p0 -> (F[1,1] p1)))",
            "WESTMapping": "p0: ((control_mode = q_heatup) & (! inv1_holds))<br/>p1: (control_mode = q_scram)",
            "R2U2Code": "((((! ((control_mode == q_heatup) && (! inv1_holds))) && (F[1,1] ((control_mode == q_heatup) && (! inv1_holds)))) -> (F[2,2] (control_mode == q_scram))) && (((TAU == 0) && ((control_mode == q_heatup) && (! inv1_holds))) -> (F[1,1] (control_mode == q_scram))))",
            "component": "DRC"
        },
        "status": "",
        "_id": "68403104-3463-11f1-b848-f314240f620d"
    },
    {
        "reqid": "DRC_T004_OPERATION_TO_SCRAM",
        "parent_reqid": "",
        "project": "PWR_HYBRID_3",
        "rationale": "",
        "comments": "",
        "fulltext": "Upon control_mode = q_operation & !inv2_holds   DRC shall at the next timepoint satisfy control_mode = q_scram",
        "semantics": {
            "type": "nasa",
            "scope": {
                "type": "null"
            },
            "condition": "regular",
            "probability": "null",
            "timing": "next",
            "response": "satisfaction",
            "variables": [
                "control_mode",
                "q_operation",
                "inv2_holds",
                "q_scram"
            ],
            "qualifier_word": "upon",
            "pre_condition": "(control_mode = q_operation & ! inv2_holds)",
            "regular_condition": "(control_mode = q_operation & ! inv2_holds)",
            "conditionTextRange": [
                0,
                44
            ],
            "component_name": "DRC",
            "componentTextRange": [
                48,
                50
            ],
            "timingTextRange": [
                58,
                78
            ],
            "post_condition": "(control_mode = q_scram)",
            "responseTextRange": [
                80,
                109
            ],
            "diagramVariables": "TC = <b><i>(control_mode = q_operation & ! inv2_holds)</i></b>, Response = <b><i>(control_mode = q_scram)</i></b>.",
            "description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: first point in the interval if <b><i>(control_mode = q_operation & ! inv2_holds)</i></b> is true and any point in the interval where <b><i>(control_mode = q_operation & ! inv2_holds)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, <b><i>(control_mode = q_scram)</i></b> must hold at the next time step.",
            "probabilistic_description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: first point in the interval if <b><i>(control_mode = q_operation & ! inv2_holds)</i></b> is true and any point in the interval where <b><i>(control_mode = q_operation & ! inv2_holds)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, with probability >=1, <b><i>(control_mode = q_scram)</i></b> must hold at the next time step.",
            "diagram": "_media/user-interface/examples/svgDiagrams/null_regular_next_satisfaction.svg",
            "scope_mode_pt": "BAD_PT",
            "scope_mode_ft": "BAD_FT",
            "regular_condition_unexp_pt": "((control_mode = q_operation) & (! inv2_holds))",
            "regular_condition_unexp_ft": "((control_mode = q_operation) & (! inv2_holds))",
            "regular_condition_unexp_pctl": "((control_mode = q_operation) & (! inv2_holds))",
            "regular_condition_SMV_pt": "((control_mode = q_operation) & (! inv2_holds))",
            "regular_condition_SMV_ft": "((control_mode = q_operation) & (! inv2_holds))",
            "regular_condition_MLTL_ft": "((control_mode = q_operation) & (! inv2_holds))",
            "regular_condition_PRISM_pctl": "((control_mode = q_operation) & (! inv2_holds))",
            "post_condition_unexp_pt": "(control_mode = q_scram)",
            "post_condition_unexp_ft": "(control_mode = q_scram)",
            "post_condition_unexp_pctl": "(control_mode = q_scram)",
            "post_condition_SMV_pt": "(control_mode = q_scram)",
            "post_condition_SMV_ft": "(control_mode = q_scram)",
            "post_condition_MLTL_ft": "(control_mode = q_scram)",
            "post_condition_PRISM_pctl": "(control_mode = q_scram)",
            "ft": "((LAST V (((! ((control_mode = q_operation) & (! inv2_holds))) & ((! LAST) & (X ((control_mode = q_operation) & (! inv2_holds))))) -> (X (LAST | (X (control_mode = q_scram)))))) & (((control_mode = q_operation) & (! inv2_holds)) -> (LAST | (X (control_mode = q_scram)))))",
            "pt": "(H ((Y (((control_mode = q_operation) & (! inv2_holds)) & (Z (! ((control_mode = q_operation) & (! inv2_holds)))))) -> ((control_mode = q_scram) | (Z FALSE))))",
            "pctl": "P>=1[((G (((! ((control_mode = q_operation) & (! inv2_holds))) & (X ((control_mode = q_operation) & (! inv2_holds)))) => (X (P>=1[(LAST | (X (control_mode = q_scram)))])))) & (((control_mode = q_operation) & (! inv2_holds)) => (P>=1[(LAST | (X (control_mode = q_scram)))])))]",
            "ptExpanded": "(H ((Y (((control_mode = q_operation) & (! inv2_holds)) & (Z (! ((control_mode = q_operation) & (! inv2_holds)))))) -> ((control_mode = q_scram) | (Z FALSE))))",
            "CoCoSpecCode": "H((YtoPre((((control_mode = q_operation) and not (inv2_holds)) and ZtoPre(not (((control_mode = q_operation) and not (inv2_holds)))))) => ((control_mode = q_scram) or ZtoPre(false))))",
            "ftExpanded": "((LAST V (((! ((control_mode = q_operation) & (! inv2_holds))) & ((! LAST) & (X ((control_mode = q_operation) & (! inv2_holds))))) -> (X (LAST | (X (control_mode = q_scram)))))) & (((control_mode = q_operation) & (! inv2_holds)) -> (LAST | (X (control_mode = q_scram)))))",
            "pctlExpanded": "P>=1[((G (((! ((control_mode = q_operation) & (! inv2_holds))) & (X ((control_mode = q_operation) & (! inv2_holds)))) => (X (P>=1[(false | (X (control_mode = q_scram)))])))) & (((control_mode = q_operation) & (! inv2_holds)) => (P>=1[(false | (X (control_mode = q_scram)))])))]",
            "ftInfAUExpanded": "((G (((! ((control_mode = q_operation) & (! inv2_holds))) & (X ((control_mode = q_operation) & (! inv2_holds)))) -> (X (X (control_mode = q_scram))))) & (((control_mode = q_operation) & (! inv2_holds)) -> (X (control_mode = q_scram))))",
            "mltlExpanded": "((G[0,M] (((! p0) & (F[1,1] p0)) -> (F[2,2] p1))) & (p0 -> (F[1,1] p1)))",
            "WESTMapping": "p0: ((control_mode = q_operation) & (! inv2_holds))<br/>p1: (control_mode = q_scram)",
            "R2U2Code": "((((! ((control_mode == q_operation) && (! inv2_holds))) && (F[1,1] ((control_mode == q_operation) && (! inv2_holds)))) -> (F[2,2] (control_mode == q_scram))) && (((TAU == 0) && ((control_mode == q_operation) && (! inv2_holds))) -> (F[1,1] (control_mode == q_scram))))",
            "component": "DRC"
        },
        "status": "",
        "_id": "68403105-3463-11f1-b848-f314240f620d"
    },
    {
        "reqid": "DRC_T005_SCRAM_TO_SHUTDOWN",
        "parent_reqid": "",
        "project": "PWR_HYBRID_3",
        "rationale": "",
        "comments": "",
        "fulltext": "Upon control_mode = q_scram & manual_reset   DRC shall at the next timepoint satisfy control_mode = q_shutdown",
        "semantics": {
            "type": "nasa",
            "scope": {
                "type": "null"
            },
            "condition": "regular",
            "probability": "null",
            "timing": "next",
            "response": "satisfaction",
            "variables": [
                "control_mode",
                "q_scram",
                "manual_reset",
                "q_shutdown"
            ],
            "qualifier_word": "upon",
            "pre_condition": "(control_mode = q_scram & manual_reset)",
            "regular_condition": "(control_mode = q_scram & manual_reset)",
            "conditionTextRange": [
                0,
                41
            ],
            "component_name": "DRC",
            "componentTextRange": [
                45,
                47
            ],
            "timingTextRange": [
                55,
                75
            ],
            "post_condition": "(control_mode = q_shutdown)",
            "responseTextRange": [
                77,
                109
            ],
            "diagramVariables": "TC = <b><i>(control_mode = q_scram & manual_reset)</i></b>, Response = <b><i>(control_mode = q_shutdown)</i></b>.",
            "description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: first point in the interval if <b><i>(control_mode = q_scram & manual_reset)</i></b> is true and any point in the interval where <b><i>(control_mode = q_scram & manual_reset)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, <b><i>(control_mode = q_shutdown)</i></b> must hold at the next time step.",
            "probabilistic_description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: first point in the interval if <b><i>(control_mode = q_scram & manual_reset)</i></b> is true and any point in the interval where <b><i>(control_mode = q_scram & manual_reset)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, with probability >=1, <b><i>(control_mode = q_shutdown)</i></b> must hold at the next time step.",
            "diagram": "_media/user-interface/examples/svgDiagrams/null_regular_next_satisfaction.svg",
            "scope_mode_pt": "BAD_PT",
            "scope_mode_ft": "BAD_FT",
            "regular_condition_unexp_pt": "((control_mode = q_scram) & manual_reset)",
            "regular_condition_unexp_ft": "((control_mode = q_scram) & manual_reset)",
            "regular_condition_unexp_pctl": "((control_mode = q_scram) & manual_reset)",
            "regular_condition_SMV_pt": "((control_mode = q_scram) & manual_reset)",
            "regular_condition_SMV_ft": "((control_mode = q_scram) & manual_reset)",
            "regular_condition_MLTL_ft": "((control_mode = q_scram) & manual_reset)",
            "regular_condition_PRISM_pctl": "((control_mode = q_scram) & manual_reset)",
            "post_condition_unexp_pt": "(control_mode = q_shutdown)",
            "post_condition_unexp_ft": "(control_mode = q_shutdown)",
            "post_condition_unexp_pctl": "(control_mode = q_shutdown)",
            "post_condition_SMV_pt": "(control_mode = q_shutdown)",
            "post_condition_SMV_ft": "(control_mode = q_shutdown)",
            "post_condition_MLTL_ft": "(control_mode = q_shutdown)",
            "post_condition_PRISM_pctl": "(control_mode = q_shutdown)",
            "ft": "((LAST V (((! ((control_mode = q_scram) & manual_reset)) & ((! LAST) & (X ((control_mode = q_scram) & manual_reset)))) -> (X (LAST | (X (control_mode = q_shutdown)))))) & (((control_mode = q_scram) & manual_reset) -> (LAST | (X (control_mode = q_shutdown)))))",
            "pt": "(H ((Y (((control_mode = q_scram) & manual_reset) & (Z (! ((control_mode = q_scram) & manual_reset))))) -> ((control_mode = q_shutdown) | (Z FALSE))))",
            "pctl": "P>=1[((G (((! ((control_mode = q_scram) & manual_reset)) & (X ((control_mode = q_scram) & manual_reset))) => (X (P>=1[(LAST | (X (control_mode = q_shutdown)))])))) & (((control_mode = q_scram) & manual_reset) => (P>=1[(LAST | (X (control_mode = q_shutdown)))])))]",
            "ptExpanded": "(H ((Y (((control_mode = q_scram) & manual_reset) & (Z (! ((control_mode = q_scram) & manual_reset))))) -> ((control_mode = q_shutdown) | (Z FALSE))))",
            "CoCoSpecCode": "H((YtoPre((((control_mode = q_scram) and manual_reset) and ZtoPre(not (((control_mode = q_scram) and manual_reset))))) => ((control_mode = q_shutdown) or ZtoPre(false))))",
            "ftExpanded": "((LAST V (((! ((control_mode = q_scram) & manual_reset)) & ((! LAST) & (X ((control_mode = q_scram) & manual_reset)))) -> (X (LAST | (X (control_mode = q_shutdown)))))) & (((control_mode = q_scram) & manual_reset) -> (LAST | (X (control_mode = q_shutdown)))))",
            "pctlExpanded": "P>=1[((G (((! ((control_mode = q_scram) & manual_reset)) & (X ((control_mode = q_scram) & manual_reset))) => (X (P>=1[(false | (X (control_mode = q_shutdown)))])))) & (((control_mode = q_scram) & manual_reset) => (P>=1[(false | (X (control_mode = q_shutdown)))])))]",
            "ftInfAUExpanded": "((G (((! ((control_mode = q_scram) & manual_reset)) & (X ((control_mode = q_scram) & manual_reset))) -> (X (X (control_mode = q_shutdown))))) & (((control_mode = q_scram) & manual_reset) -> (X (control_mode = q_shutdown))))",
            "mltlExpanded": "((G[0,M] (((! p0) & (F[1,1] p0)) -> (F[2,2] p1))) & (p0 -> (F[1,1] p1)))",
            "WESTMapping": "p0: ((control_mode = q_scram) & manual_reset)<br/>p1: (control_mode = q_shutdown)",
            "R2U2Code": "((((! ((control_mode == q_scram) && manual_reset)) && (F[1,1] ((control_mode == q_scram) && manual_reset))) -> (F[2,2] (control_mode == q_shutdown))) && (((TAU == 0) && ((control_mode == q_scram) && manual_reset)) -> (F[1,1] (control_mode == q_shutdown))))",
            "component": "DRC"
        },
        "status": "",
        "_id": "68403106-3463-11f1-b848-f314240f620d"
    },
    {
        "reqid": "DRC_S001_SHUTDOWN_STAY",
        "parent_reqid": "",
        "project": "PWR_HYBRID_3",
        "rationale": "",
        "comments": "",
        "fulltext": "Whenever control_mode = q_shutdown & !t_avg_above_min   DRC shall at the next timepoint satisfy control_mode = q_shutdown",
        "semantics": {
            "type": "nasa",
            "scope": {
                "type": "null"
            },
            "condition": "holding",
            "probability": "null",
            "timing": "next",
            "response": "satisfaction",
            "variables": [
                "control_mode",
                "q_shutdown",
                "t_avg_above_min"
            ],
            "qualifier_word": "whenever",
            "pre_condition": "(control_mode = q_shutdown & ! t_avg_above_min)",
            "regular_condition": "(control_mode = q_shutdown & ! t_avg_above_min)",
            "conditionTextRange": [
                0,
                52
            ],
            "component_name": "DRC",
            "componentTextRange": [
                56,
                58
            ],
            "timingTextRange": [
                66,
                86
            ],
            "post_condition": "(control_mode = q_shutdown)",
            "responseTextRange": [
                88,
                120
            ],
            "diagramVariables": "CC = <b><i>(control_mode = q_shutdown & ! t_avg_above_min)</i></b>, Response = <b><i>(control_mode = q_shutdown)</i></b>.",
            "description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: every point in the interval where <b><i>(control_mode = q_shutdown & ! t_avg_above_min)</i></b> is true.<br>REQUIRED BEHAVIOR: for every trigger, <b><i>(control_mode = q_shutdown)</i></b> must hold at the next time step.",
            "probabilistic_description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: every point in the interval where <b><i>(control_mode = q_shutdown & ! t_avg_above_min)</i></b> is true.<br>REQUIRED BEHAVIOR: for every trigger, with probability >=1, <b><i>(control_mode = q_shutdown)</i></b> must hold at the next time step.",
            "diagram": "_media/user-interface/examples/svgDiagrams/null_holding_next_satisfaction.svg",
            "scope_mode_pt": "BAD_PT",
            "scope_mode_ft": "BAD_FT",
            "regular_condition_unexp_pt": "((control_mode = q_shutdown) & (! t_avg_above_min))",
            "regular_condition_unexp_ft": "((control_mode = q_shutdown) & (! t_avg_above_min))",
            "regular_condition_unexp_pctl": "((control_mode = q_shutdown) & (! t_avg_above_min))",
            "regular_condition_SMV_pt": "((control_mode = q_shutdown) & (! t_avg_above_min))",
            "regular_condition_SMV_ft": "((control_mode = q_shutdown) & (! t_avg_above_min))",
            "regular_condition_MLTL_ft": "((control_mode = q_shutdown) & (! t_avg_above_min))",
            "regular_condition_PRISM_pctl": "((control_mode = q_shutdown) & (! t_avg_above_min))",
            "post_condition_unexp_pt": "(control_mode = q_shutdown)",
            "post_condition_unexp_ft": "(control_mode = q_shutdown)",
            "post_condition_unexp_pctl": "(control_mode = q_shutdown)",
            "post_condition_SMV_pt": "(control_mode = q_shutdown)",
            "post_condition_SMV_ft": "(control_mode = q_shutdown)",
            "post_condition_MLTL_ft": "(control_mode = q_shutdown)",
            "post_condition_PRISM_pctl": "(control_mode = q_shutdown)",
            "ft": "(LAST V (((control_mode = q_shutdown) & (! t_avg_above_min)) -> (LAST | (X (control_mode = q_shutdown)))))",
            "pt": "(H ((Y ((control_mode = q_shutdown) & (! t_avg_above_min))) -> ((control_mode = q_shutdown) | (Z FALSE))))",
            "pctl": "P>=1[(G (((control_mode = q_shutdown) & (! t_avg_above_min)) => (P>=1[(LAST | (X (control_mode = q_shutdown)))])))]",
            "ptExpanded": "(H ((Y ((control_mode = q_shutdown) & (! t_avg_above_min))) -> ((control_mode = q_shutdown) | (Z FALSE))))",
            "CoCoSpecCode": "H((YtoPre(((control_mode = q_shutdown) and not (t_avg_above_min))) => ((control_mode = q_shutdown) or ZtoPre(false))))",
            "ftExpanded": "(LAST V (((control_mode = q_shutdown) & (! t_avg_above_min)) -> (LAST | (X (control_mode = q_shutdown)))))",
            "pctlExpanded": "P>=1[(G (((control_mode = q_shutdown) & (! t_avg_above_min)) => (P>=1[(false | (X (control_mode = q_shutdown)))])))]",
            "ftInfAUExpanded": "(G (((control_mode = q_shutdown) & (! t_avg_above_min)) -> (X (control_mode = q_shutdown))))",
            "mltlExpanded": "(G[0,M] (p0 -> (F[1,1] p1)))",
            "WESTMapping": "p0: ((control_mode = q_shutdown) & (! t_avg_above_min))<br/>p1: (control_mode = q_shutdown)",
            "R2U2Code": "(((control_mode == q_shutdown) && (! t_avg_above_min)) -> (F[1,1] (control_mode == q_shutdown)))",
            "component": "DRC"
        },
        "status": "",
        "_id": "68403107-3463-11f1-b848-f314240f620d"
    },
    {
        "reqid": "DRC_S002_HEATUP_STAY",
        "parent_reqid": "",
        "project": "PWR_HYBRID_3",
        "rationale": "",
        "comments": "",
        "fulltext": "Whenever control_mode = q_heatup & inv1_holds & !(t_avg_in_range & p_above_crit)   DRC shall at the next timepoint satisfy control_mode = q_heatup",
        "semantics": {
            "type": "nasa",
            "scope": {
                "type": "null"
            },
            "condition": "holding",
            "probability": "null",
            "timing": "next",
            "response": "satisfaction",
            "variables": [
                "control_mode",
                "q_heatup",
                "inv1_holds",
                "t_avg_in_range",
                "p_above_crit"
            ],
            "qualifier_word": "whenever",
            "pre_condition": "(control_mode = q_heatup & inv1_holds & ! ( t_avg_in_range & p_above_crit ))",
            "regular_condition": "(control_mode = q_heatup & inv1_holds & ! ( t_avg_in_range & p_above_crit ))",
            "conditionTextRange": [
                0,
                79
            ],
            "component_name": "DRC",
            "componentTextRange": [
                83,
                85
            ],
            "timingTextRange": [
                93,
                113
            ],
            "post_condition": "(control_mode = q_heatup)",
            "responseTextRange": [
                115,
                145
            ],
            "diagramVariables": "CC = <b><i>(control_mode = q_heatup & inv1_holds & ! ( t_avg_in_range & p_above_crit ))</i></b>, Response = <b><i>(control_mode = q_heatup)</i></b>.",
            "description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: every point in the interval where <b><i>(control_mode = q_heatup & inv1_holds & ! ( t_avg_in_range & p_above_crit ))</i></b> is true.<br>REQUIRED BEHAVIOR: for every trigger, <b><i>(control_mode = q_heatup)</i></b> must hold at the next time step.",
            "probabilistic_description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: every point in the interval where <b><i>(control_mode = q_heatup & inv1_holds & ! ( t_avg_in_range & p_above_crit ))</i></b> is true.<br>REQUIRED BEHAVIOR: for every trigger, with probability >=1, <b><i>(control_mode = q_heatup)</i></b> must hold at the next time step.",
            "diagram": "_media/user-interface/examples/svgDiagrams/null_holding_next_satisfaction.svg",
            "scope_mode_pt": "BAD_PT",
            "scope_mode_ft": "BAD_FT",
            "regular_condition_unexp_pt": "(((control_mode = q_heatup) & inv1_holds) & (! (t_avg_in_range & p_above_crit)))",
            "regular_condition_unexp_ft": "(((control_mode = q_heatup) & inv1_holds) & (! (t_avg_in_range & p_above_crit)))",
            "regular_condition_unexp_pctl": "(((control_mode = q_heatup) & inv1_holds) & (! (t_avg_in_range & p_above_crit)))",
            "regular_condition_SMV_pt": "(((control_mode = q_heatup) & inv1_holds) & (! (t_avg_in_range & p_above_crit)))",
            "regular_condition_SMV_ft": "(((control_mode = q_heatup) & inv1_holds) & (! (t_avg_in_range & p_above_crit)))",
            "regular_condition_MLTL_ft": "(((control_mode = q_heatup) & inv1_holds) & (! (t_avg_in_range & p_above_crit)))",
            "regular_condition_PRISM_pctl": "(((control_mode = q_heatup) & inv1_holds) & (! (t_avg_in_range & p_above_crit)))",
            "post_condition_unexp_pt": "(control_mode = q_heatup)",
            "post_condition_unexp_ft": "(control_mode = q_heatup)",
            "post_condition_unexp_pctl": "(control_mode = q_heatup)",
            "post_condition_SMV_pt": "(control_mode = q_heatup)",
            "post_condition_SMV_ft": "(control_mode = q_heatup)",
            "post_condition_MLTL_ft": "(control_mode = q_heatup)",
            "post_condition_PRISM_pctl": "(control_mode = q_heatup)",
            "ft": "(LAST V ((((control_mode = q_heatup) & inv1_holds) & (! (t_avg_in_range & p_above_crit))) -> (LAST | (X (control_mode = q_heatup)))))",
            "pt": "(H ((Y (((control_mode = q_heatup) & inv1_holds) & (! (t_avg_in_range & p_above_crit)))) -> ((control_mode = q_heatup) | (Z FALSE))))",
            "pctl": "P>=1[(G ((((control_mode = q_heatup) & inv1_holds) & (! (t_avg_in_range & p_above_crit))) => (P>=1[(LAST | (X (control_mode = q_heatup)))])))]",
            "ptExpanded": "(H ((Y (((control_mode = q_heatup) & inv1_holds) & (! (t_avg_in_range & p_above_crit)))) -> ((control_mode = q_heatup) | (Z FALSE))))",
            "CoCoSpecCode": "H((YtoPre((((control_mode = q_heatup) and inv1_holds) and not ((t_avg_in_range and p_above_crit)))) => ((control_mode = q_heatup) or ZtoPre(false))))",
            "ftExpanded": "(LAST V ((((control_mode = q_heatup) & inv1_holds) & (! (t_avg_in_range & p_above_crit))) -> (LAST | (X (control_mode = q_heatup)))))",
            "pctlExpanded": "P>=1[(G ((((control_mode = q_heatup) & inv1_holds) & (! (t_avg_in_range & p_above_crit))) => (P>=1[(false | (X (control_mode = q_heatup)))])))]",
            "ftInfAUExpanded": "(G ((((control_mode = q_heatup) & inv1_holds) & (! (t_avg_in_range & p_above_crit))) -> (X (control_mode = q_heatup))))",
            "mltlExpanded": "(G[0,M] (p0 -> (F[1,1] p1)))",
            "WESTMapping": "p0: (((control_mode = q_heatup) & inv1_holds) & (! (t_avg_in_range & p_above_crit)))<br/>p1: (control_mode = q_heatup)",
            "R2U2Code": "((((control_mode == q_heatup) && inv1_holds) && (! (t_avg_in_range && p_above_crit))) -> (F[1,1] (control_mode == q_heatup)))",
            "component": "DRC"
        },
        "status": "",
        "_id": "68403108-3463-11f1-b848-f314240f620d"
    },
    {
        "reqid": "DRC_S003_OPERATION_STAY",
        "parent_reqid": "",
        "project": "PWR_HYBRID_3",
        "rationale": "",
        "comments": "",
        "fulltext": "Whenever control_mode = q_operation & inv2_holds  DRC shall at the next timepoint satisfy control_mode = q_operation ",
        "semantics": {
            "type": "nasa",
            "scope": {
                "type": "null"
            },
            "condition": "holding",
            "probability": "null",
            "timing": "next",
            "response": "satisfaction",
            "variables": [
                "control_mode",
                "q_operation",
                "inv2_holds"
            ],
            "qualifier_word": "whenever",
            "pre_condition": "(control_mode = q_operation & inv2_holds)",
            "regular_condition": "(control_mode = q_operation & inv2_holds)",
            "conditionTextRange": [
                0,
                47
            ],
            "component_name": "DRC",
            "componentTextRange": [
                50,
                52
            ],
            "timingTextRange": [
                60,
                80
            ],
            "post_condition": "(control_mode = q_operation)",
            "responseTextRange": [
                82,
                115
            ],
            "diagramVariables": "CC = <b><i>(control_mode = q_operation & inv2_holds)</i></b>, Response = <b><i>(control_mode = q_operation)</i></b>.",
            "description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: every point in the interval where <b><i>(control_mode = q_operation & inv2_holds)</i></b> is true.<br>REQUIRED BEHAVIOR: for every trigger, <b><i>(control_mode = q_operation)</i></b> must hold at the next time step.",
            "probabilistic_description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: every point in the interval where <b><i>(control_mode = q_operation & inv2_holds)</i></b> is true.<br>REQUIRED BEHAVIOR: for every trigger, with probability >=1, <b><i>(control_mode = q_operation)</i></b> must hold at the next time step.",
            "diagram": "_media/user-interface/examples/svgDiagrams/null_holding_next_satisfaction.svg",
            "scope_mode_pt": "BAD_PT",
            "scope_mode_ft": "BAD_FT",
            "regular_condition_unexp_pt": "((control_mode = q_operation) & inv2_holds)",
            "regular_condition_unexp_ft": "((control_mode = q_operation) & inv2_holds)",
            "regular_condition_unexp_pctl": "((control_mode = q_operation) & inv2_holds)",
            "regular_condition_SMV_pt": "((control_mode = q_operation) & inv2_holds)",
            "regular_condition_SMV_ft": "((control_mode = q_operation) & inv2_holds)",
            "regular_condition_MLTL_ft": "((control_mode = q_operation) & inv2_holds)",
            "regular_condition_PRISM_pctl": "((control_mode = q_operation) & inv2_holds)",
            "post_condition_unexp_pt": "(control_mode = q_operation)",
            "post_condition_unexp_ft": "(control_mode = q_operation)",
            "post_condition_unexp_pctl": "(control_mode = q_operation)",
            "post_condition_SMV_pt": "(control_mode = q_operation)",
            "post_condition_SMV_ft": "(control_mode = q_operation)",
            "post_condition_MLTL_ft": "(control_mode = q_operation)",
            "post_condition_PRISM_pctl": "(control_mode = q_operation)",
            "ft": "(LAST V (((control_mode = q_operation) & inv2_holds) -> (LAST | (X (control_mode = q_operation)))))",
            "pt": "(H ((Y ((control_mode = q_operation) & inv2_holds)) -> ((control_mode = q_operation) | (Z FALSE))))",
            "pctl": "P>=1[(G (((control_mode = q_operation) & inv2_holds) => (P>=1[(LAST | (X (control_mode = q_operation)))])))]",
            "ptExpanded": "(H ((Y ((control_mode = q_operation) & inv2_holds)) -> ((control_mode = q_operation) | (Z FALSE))))",
            "CoCoSpecCode": "H((YtoPre(((control_mode = q_operation) and inv2_holds)) => ((control_mode = q_operation) or ZtoPre(false))))",
            "ftExpanded": "(LAST V (((control_mode = q_operation) & inv2_holds) -> (LAST | (X (control_mode = q_operation)))))",
            "pctlExpanded": "P>=1[(G (((control_mode = q_operation) & inv2_holds) => (P>=1[(false | (X (control_mode = q_operation)))])))]",
            "ftInfAUExpanded": "(G (((control_mode = q_operation) & inv2_holds) -> (X (control_mode = q_operation))))",
            "mltlExpanded": "(G[0,M] (p0 -> (F[1,1] p1)))",
            "WESTMapping": "p0: ((control_mode = q_operation) & inv2_holds)<br/>p1: (control_mode = q_operation)",
            "R2U2Code": "(((control_mode == q_operation) && inv2_holds) -> (F[1,1] (control_mode == q_operation)))",
            "component": "DRC"
        },
        "status": "",
        "_id": "68403109-3463-11f1-b848-f314240f620d"
    },
    {
        "reqid": "DRC_I001_INIT_SHUTDOWN",
        "parent_reqid": "",
        "project": "PWR_HYBRID_3",
        "rationale": "",
        "comments": "",
        "fulltext": "DRC shall immediately satisfy control_mode = q_shutdown",
        "semantics": {
            "type": "nasa",
            "scope": {
                "type": "null"
            },
            "condition": "null",
            "probability": "null",
            "timing": "immediately",
            "response": "satisfaction",
            "variables": [
                "control_mode",
                "q_shutdown"
            ],
            "component_name": "DRC",
            "componentTextRange": [
                0,
                2
            ],
            "timingTextRange": [
                10,
                20
            ],
            "post_condition": "(control_mode = q_shutdown)",
            "responseTextRange": [
                22,
                54
            ],
            "diagramVariables": "Response = <b><i>(control_mode = q_shutdown)</i></b>.",
            "description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: first point in the interval.<br>REQUIRED BEHAVIOR: for every trigger, if trigger holds then <b><i>(control_mode = q_shutdown)</i></b> also holds at the same time point.",
            "probabilistic_description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: first point in the interval.<br>REQUIRED BEHAVIOR: for every trigger, with probability >=1, if trigger holds then <b><i>(control_mode = q_shutdown)</i></b> also holds at the same time point.",
            "diagram": "_media/user-interface/examples/svgDiagrams/null_null_immediately_satisfaction.svg",
            "scope_mode_pt": "BAD_PT",
            "scope_mode_ft": "BAD_FT",
            "post_condition_unexp_pt": "(control_mode = q_shutdown)",
            "post_condition_unexp_ft": "(control_mode = q_shutdown)",
            "post_condition_unexp_pctl": "(control_mode = q_shutdown)",
            "post_condition_SMV_pt": "(control_mode = q_shutdown)",
            "post_condition_SMV_ft": "(control_mode = q_shutdown)",
            "post_condition_MLTL_ft": "(control_mode = q_shutdown)",
            "post_condition_PRISM_pctl": "(control_mode = q_shutdown)",
            "ft": "(control_mode = q_shutdown)",
            "pt": "(H ((Z FALSE) -> (control_mode = q_shutdown)))",
            "pctl": "(P>=1[(control_mode = q_shutdown)])",
            "ptExpanded": "(H ((Z FALSE) -> (control_mode = q_shutdown)))",
            "CoCoSpecCode": "H((ZtoPre(false) => (control_mode = q_shutdown)))",
            "ftExpanded": "(control_mode = q_shutdown)",
            "pctlExpanded": "(P>=1[(control_mode = q_shutdown)])",
            "ftInfAUExpanded": "(control_mode = q_shutdown)",
            "mltlExpanded": "p0",
            "WESTMapping": "p0: (control_mode = q_shutdown)",
            "R2U2Code": "((TAU == 0) -> (control_mode == q_shutdown))",
            "component": "DRC"
        },
        "status": "",
        "_id": "6840310a-3463-11f1-b848-f314240f620d"
    }
]