{
    "requirements": [
        {
            "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",
            "status": "",
            "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"
            },
            "_id": "00151d40-3439-11f1-9e90-533f2b59d63b"
        },
        {
            "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",
            "status": "",
            "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"
            },
            "_id": "07c92900-3439-11f1-9e90-533f2b59d63b"
        },
        {
            "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",
            "status": "",
            "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"
            },
            "_id": "0ee142e0-3439-11f1-9e90-533f2b59d63b"
        },
        {
            "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",
            "status": "",
            "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"
            },
            "_id": "0f592770-3438-11f1-9e90-533f2b59d63b"
        },
        {
            "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",
            "status": "",
            "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"
            },
            "_id": "1708a9e0-3439-11f1-9e90-533f2b59d63b"
        },
        {
            "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",
            "status": "",
            "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"
            },
            "_id": "1f626b80-3439-11f1-9e90-533f2b59d63b"
        },
        {
            "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",
            "status": "",
            "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"
            },
            "_id": "268581e0-3439-11f1-9e90-533f2b59d63b"
        },
        {
            "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",
            "status": "",
            "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"
            },
            "_id": "27113c90-3438-11f1-9e90-533f2b59d63b"
        },
        {
            "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",
            "status": "",
            "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"
            },
            "_id": "de451bc0-3438-11f1-9e90-533f2b59d63b"
        },
        {
            "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 ",
            "status": "",
            "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"
            },
            "_id": "ec1666a0-3438-11f1-9e90-533f2b59d63b"
        },
        {
            "reqid": "DRC_I001_INIT_SHUTDOWN",
            "parent_reqid": "",
            "project": "PWR_HYBRID_3",
            "rationale": "",
            "comments": "",
            "fulltext": "DRC shall immediately satisfy control_mode = q_shutdown",
            "status": "",
            "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"
            },
            "_id": "f21c42a0-3437-11f1-9e90-533f2b59d63b"
        }
    ],
    "variables": [
        {
            "project": "FSM",
            "component_name": "sw",
            "variable_name": "P",
            "reqs": [
                "L1"
            ],
            "otherDeps": [],
            "dataType": "",
            "idType": "",
            "description": "",
            "assignment": "",
            "modeRequirement": "",
            "model": false,
            "modelComponent": "",
            "model_id": "",
            "_id": "FSMswP"
        },
        {
            "project": "FSM",
            "component_name": "sw",
            "variable_name": "R",
            "reqs": [
                "L1"
            ],
            "otherDeps": [],
            "dataType": "",
            "idType": "",
            "description": "",
            "assignment": "",
            "modeRequirement": "",
            "model": false,
            "modelComponent": "",
            "model_id": "",
            "_id": "FSMswR"
        },
        {
            "project": "PWR_HYBRID_3",
            "component_name": "DRC",
            "variable_name": "control_mode",
            "reqs": [
                "00151d40-3439-11f1-9e90-533f2b59d63b",
                "07c92900-3439-11f1-9e90-533f2b59d63b",
                "0ee142e0-3439-11f1-9e90-533f2b59d63b",
                "0f592770-3438-11f1-9e90-533f2b59d63b",
                "1708a9e0-3439-11f1-9e90-533f2b59d63b",
                "1f626b80-3439-11f1-9e90-533f2b59d63b",
                "268581e0-3439-11f1-9e90-533f2b59d63b",
                "27113c90-3438-11f1-9e90-533f2b59d63b",
                "de451bc0-3438-11f1-9e90-533f2b59d63b",
                "ec1666a0-3438-11f1-9e90-533f2b59d63b",
                "f21c42a0-3437-11f1-9e90-533f2b59d63b"
            ],
            "dataType": "integer",
            "idType": "Output",
            "moduleName": "",
            "description": "",
            "assignment": "",
            "assignmentVariables": [],
            "copilotAssignment": "",
            "r2u2Assignment": "",
            "smvAssignment": "",
            "smvAssignmentVariables": [],
            "modeRequirement": "",
            "modeldoc": false,
            "modeldoc_id": "",
            "modeldoc_vectorIndex": null,
            "modelComponent": "",
            "completed": true,
            "r2u2Completed": true,
            "smvCompleted": false,
            "_id": "PWR_HYBRID_3DRCcontrol_mode"
        },
        {
            "project": "PWR_HYBRID_3",
            "component_name": "DRC",
            "variable_name": "inv1_holds",
            "reqs": [
                "1708a9e0-3439-11f1-9e90-533f2b59d63b",
                "de451bc0-3438-11f1-9e90-533f2b59d63b",
                "0ee142e0-3439-11f1-9e90-533f2b59d63b"
            ],
            "dataType": "boolean",
            "idType": "Input",
            "moduleName": "",
            "description": "",
            "assignment": "",
            "assignmentVariables": [],
            "copilotAssignment": "",
            "r2u2Assignment": "",
            "smvAssignment": "",
            "smvAssignmentVariables": [],
            "modeRequirement": "",
            "modeldoc": false,
            "modeldoc_id": "",
            "modeldoc_vectorIndex": null,
            "modelComponent": "",
            "completed": true,
            "r2u2Completed": true,
            "smvCompleted": true,
            "_id": "PWR_HYBRID_3DRCinv1_holds"
        },
        {
            "project": "PWR_HYBRID_3",
            "component_name": "DRC",
            "variable_name": "inv2_holds",
            "reqs": [
                "1f626b80-3439-11f1-9e90-533f2b59d63b",
                "ec1666a0-3438-11f1-9e90-533f2b59d63b"
            ],
            "dataType": "boolean",
            "idType": "Input",
            "moduleName": "",
            "description": "",
            "assignment": "",
            "assignmentVariables": [],
            "copilotAssignment": "",
            "r2u2Assignment": "",
            "smvAssignment": "",
            "smvAssignmentVariables": [],
            "modeRequirement": "",
            "modeldoc": false,
            "modeldoc_id": "",
            "modeldoc_vectorIndex": null,
            "modelComponent": "",
            "completed": true,
            "r2u2Completed": true,
            "smvCompleted": true,
            "_id": "PWR_HYBRID_3DRCinv2_holds"
        },
        {
            "project": "PWR_HYBRID_3",
            "component_name": "DRC",
            "variable_name": "manual_reset",
            "reqs": [
                "00151d40-3439-11f1-9e90-533f2b59d63b",
                "268581e0-3439-11f1-9e90-533f2b59d63b"
            ],
            "dataType": "boolean",
            "idType": "Input",
            "moduleName": "",
            "description": "",
            "assignment": "",
            "assignmentVariables": [],
            "copilotAssignment": "",
            "r2u2Assignment": "",
            "smvAssignment": "",
            "smvAssignmentVariables": [],
            "modeRequirement": "",
            "modeldoc": false,
            "modeldoc_id": "",
            "modeldoc_vectorIndex": null,
            "modelComponent": "",
            "completed": true,
            "r2u2Completed": true,
            "smvCompleted": true,
            "_id": "PWR_HYBRID_3DRCmanual_reset"
        },
        {
            "project": "PWR_HYBRID_3",
            "component_name": "DRC",
            "variable_name": "p_above_crit",
            "reqs": [
                "0ee142e0-3439-11f1-9e90-533f2b59d63b",
                "de451bc0-3438-11f1-9e90-533f2b59d63b"
            ],
            "dataType": "boolean",
            "idType": "Input",
            "moduleName": "",
            "description": "",
            "assignment": "",
            "assignmentVariables": [],
            "copilotAssignment": "",
            "r2u2Assignment": "",
            "smvAssignment": "",
            "smvAssignmentVariables": [],
            "modeRequirement": "",
            "modeldoc": false,
            "modeldoc_id": "",
            "modeldoc_vectorIndex": null,
            "modelComponent": "",
            "completed": true,
            "r2u2Completed": true,
            "smvCompleted": true,
            "_id": "PWR_HYBRID_3DRCp_above_crit"
        },
        {
            "project": "PWR_HYBRID_3",
            "component_name": "DRC",
            "variable_name": "q_heatup",
            "reqs": [
                "07c92900-3439-11f1-9e90-533f2b59d63b",
                "0ee142e0-3439-11f1-9e90-533f2b59d63b",
                "0f592770-3438-11f1-9e90-533f2b59d63b",
                "1708a9e0-3439-11f1-9e90-533f2b59d63b",
                "de451bc0-3438-11f1-9e90-533f2b59d63b"
            ],
            "dataType": "integer",
            "idType": "Internal",
            "moduleName": "",
            "description": "",
            "assignment": "1",
            "assignmentVariables": [],
            "copilotAssignment": "",
            "r2u2Assignment": "",
            "smvAssignment": "",
            "smvAssignmentVariables": [],
            "modeRequirement": "",
            "modeldoc": false,
            "modeldoc_id": "",
            "modeldoc_vectorIndex": null,
            "modelComponent": "",
            "completed": true,
            "r2u2Completed": false,
            "smvCompleted": false,
            "_id": "PWR_HYBRID_3DRCq_heatup"
        },
        {
            "project": "PWR_HYBRID_3",
            "component_name": "DRC",
            "variable_name": "q_operation",
            "reqs": [
                "0ee142e0-3439-11f1-9e90-533f2b59d63b",
                "0f592770-3438-11f1-9e90-533f2b59d63b",
                "1f626b80-3439-11f1-9e90-533f2b59d63b",
                "ec1666a0-3438-11f1-9e90-533f2b59d63b"
            ],
            "dataType": "integer",
            "idType": "Internal",
            "moduleName": "",
            "description": "",
            "assignment": "2",
            "assignmentVariables": [],
            "copilotAssignment": "",
            "r2u2Assignment": "",
            "smvAssignment": "",
            "smvAssignmentVariables": [],
            "modeRequirement": "",
            "modeldoc": false,
            "modeldoc_id": "",
            "modeldoc_vectorIndex": null,
            "modelComponent": "",
            "completed": true,
            "r2u2Completed": false,
            "smvCompleted": false,
            "_id": "PWR_HYBRID_3DRCq_operation"
        },
        {
            "project": "PWR_HYBRID_3",
            "component_name": "DRC",
            "variable_name": "q_scram",
            "reqs": [
                "00151d40-3439-11f1-9e90-533f2b59d63b",
                "0f592770-3438-11f1-9e90-533f2b59d63b",
                "1708a9e0-3439-11f1-9e90-533f2b59d63b",
                "1f626b80-3439-11f1-9e90-533f2b59d63b",
                "268581e0-3439-11f1-9e90-533f2b59d63b"
            ],
            "dataType": "integer",
            "idType": "Internal",
            "moduleName": "",
            "description": "",
            "assignment": "3",
            "assignmentVariables": [],
            "copilotAssignment": "",
            "r2u2Assignment": "",
            "smvAssignment": "",
            "smvAssignmentVariables": [],
            "modeRequirement": "",
            "modeldoc": false,
            "modeldoc_id": "",
            "modeldoc_vectorIndex": null,
            "modelComponent": "",
            "completed": true,
            "r2u2Completed": false,
            "smvCompleted": false,
            "_id": "PWR_HYBRID_3DRCq_scram"
        },
        {
            "project": "PWR_HYBRID_3",
            "component_name": "DRC",
            "variable_name": "q_shutdown",
            "reqs": [
                "07c92900-3439-11f1-9e90-533f2b59d63b",
                "0f592770-3438-11f1-9e90-533f2b59d63b",
                "268581e0-3439-11f1-9e90-533f2b59d63b",
                "27113c90-3438-11f1-9e90-533f2b59d63b",
                "f21c42a0-3437-11f1-9e90-533f2b59d63b"
            ],
            "dataType": "integer",
            "idType": "Internal",
            "moduleName": "",
            "description": "",
            "assignment": "0",
            "assignmentVariables": [],
            "copilotAssignment": "",
            "r2u2Assignment": "",
            "smvAssignment": "",
            "smvAssignmentVariables": [],
            "modeRequirement": "",
            "modeldoc": false,
            "modeldoc_id": "",
            "modeldoc_vectorIndex": null,
            "modelComponent": "",
            "completed": true,
            "r2u2Completed": false,
            "smvCompleted": false,
            "_id": "PWR_HYBRID_3DRCq_shutdown"
        },
        {
            "project": "PWR_HYBRID_3",
            "component_name": "DRC",
            "variable_name": "t_avg_above_min",
            "reqs": [
                "07c92900-3439-11f1-9e90-533f2b59d63b",
                "27113c90-3438-11f1-9e90-533f2b59d63b"
            ],
            "dataType": "boolean",
            "idType": "Input",
            "moduleName": "",
            "description": "",
            "assignment": "",
            "assignmentVariables": [],
            "copilotAssignment": "",
            "r2u2Assignment": "",
            "smvAssignment": "",
            "smvAssignmentVariables": [],
            "modeRequirement": "",
            "modeldoc": false,
            "modeldoc_id": "",
            "modeldoc_vectorIndex": null,
            "modelComponent": "",
            "completed": true,
            "r2u2Completed": true,
            "smvCompleted": true,
            "_id": "PWR_HYBRID_3DRCt_avg_above_min"
        },
        {
            "project": "PWR_HYBRID_3",
            "component_name": "DRC",
            "variable_name": "t_avg_in_range",
            "reqs": [
                "0ee142e0-3439-11f1-9e90-533f2b59d63b",
                "de451bc0-3438-11f1-9e90-533f2b59d63b"
            ],
            "dataType": "boolean",
            "idType": "Input",
            "moduleName": "",
            "description": "",
            "assignment": "",
            "assignmentVariables": [],
            "copilotAssignment": "",
            "r2u2Assignment": "",
            "smvAssignment": "",
            "smvAssignmentVariables": [],
            "modeRequirement": "",
            "modeldoc": false,
            "modeldoc_id": "",
            "modeldoc_vectorIndex": null,
            "modelComponent": "",
            "completed": true,
            "r2u2Completed": true,
            "smvCompleted": true,
            "_id": "PWR_HYBRID_3DRCt_avg_in_range"
        },
        {
            "project": "Liquid_mixer",
            "modeldoc": true,
            "variable_name": "emergencybutton",
            "portType": "Inport",
            "portNumber": "",
            "component_name": "liquidmixer",
            "tool": "Simulink",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "width": 1,
            "fretComponent": "liquid_mixer",
            "_id": "emergencybutton"
        },
        {
            "component_name": "fsm_12B/FiniteStateMachine",
            "dataType": [
                "double"
            ],
            "dimensions": [
                1,
                1
            ],
            "modeldoc": true,
            "portNumber": "2",
            "portType": "Outport",
            "project": "FSM",
            "tool": "Simulink",
            "variable_name": "SENSTATE",
            "width": 1,
            "fretComponent": "FSM",
            "_id": "fsm_12B/FiniteStateMachine/SENSTATE"
        },
        {
            "component_name": "fsm_12B/FiniteStateMachine",
            "dataType": [
                "double"
            ],
            "dimensions": [
                1,
                1
            ],
            "modeldoc": true,
            "portNumber": "1",
            "portType": "Outport",
            "project": "FSM",
            "tool": "Simulink",
            "variable_name": "STATE",
            "width": 1,
            "fretComponent": "FSM",
            "_id": "fsm_12B/FiniteStateMachine/STATE"
        },
        {
            "component_name": "fsm_12B/FiniteStateMachine",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "modeldoc": true,
            "portNumber": "2",
            "portType": "Inport",
            "project": "FSM",
            "tool": "Simulink",
            "variable_name": "apfail",
            "width": 1,
            "fretComponent": "FSM",
            "_id": "fsm_12B/FiniteStateMachine/apfail"
        },
        {
            "component_name": "fsm_12B/FiniteStateMachine",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "modeldoc": true,
            "portNumber": "4",
            "portType": "Inport",
            "project": "FSM",
            "tool": "Simulink",
            "variable_name": "good",
            "width": 1,
            "fretComponent": "FSM",
            "_id": "fsm_12B/FiniteStateMachine/good"
        },
        {
            "component_name": "fsm_12B/FiniteStateMachine",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "modeldoc": true,
            "portNumber": "4",
            "portType": "Inport",
            "project": "FSM",
            "tool": "Simulink",
            "variable_name": "limits",
            "width": 1,
            "fretComponent": "FSM",
            "_id": "fsm_12B/FiniteStateMachine/limits"
        },
        {
            "component_name": "fsm_12B/FiniteStateMachine",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "modeldoc": true,
            "portNumber": "1",
            "portType": "Outport",
            "project": "FSM",
            "tool": "Simulink",
            "variable_name": "pullup",
            "width": 1,
            "fretComponent": "FSM",
            "_id": "fsm_12B/FiniteStateMachine/pullup"
        },
        {
            "component_name": "fsm_12B/FiniteStateMachine",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "modeldoc": true,
            "portNumber": "2",
            "portType": "Inport",
            "project": "FSM",
            "tool": "Simulink",
            "variable_name": "request",
            "width": 1,
            "fretComponent": "FSM",
            "_id": "fsm_12B/FiniteStateMachine/request"
        },
        {
            "component_name": "fsm_12B/FiniteStateMachine",
            "dataType": [
                "double"
            ],
            "dimensions": [
                1,
                1
            ],
            "modeldoc": true,
            "portNumber": "4",
            "portType": "Inport",
            "project": "FSM",
            "tool": "Simulink",
            "variable_name": "senstate",
            "width": 1,
            "fretComponent": "FSM",
            "_id": "fsm_12B/FiniteStateMachine/senstate"
        },
        {
            "component_name": "fsm_12B/FiniteStateMachine",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "modeldoc": true,
            "portNumber": "1",
            "portType": "Inport",
            "project": "FSM",
            "tool": "Simulink",
            "variable_name": "standby",
            "width": 1,
            "fretComponent": "FSM",
            "_id": "fsm_12B/FiniteStateMachine/standby"
        },
        {
            "component_name": "fsm_12B/FiniteStateMachine",
            "dataType": [
                "double"
            ],
            "dimensions": [
                1,
                1
            ],
            "modeldoc": true,
            "portNumber": "5",
            "portType": "Inport",
            "project": "FSM",
            "tool": "Simulink",
            "variable_name": "state",
            "width": 1,
            "fretComponent": "FSM",
            "_id": "fsm_12B/FiniteStateMachine/state"
        },
        {
            "component_name": "fsm_12B/FiniteStateMachine",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "modeldoc": true,
            "portNumber": "3",
            "portType": "Inport",
            "project": "FSM",
            "tool": "Simulink",
            "variable_name": "supported",
            "width": 1,
            "fretComponent": "FSM",
            "_id": "fsm_12B/FiniteStateMachine/supported"
        },
        {
            "component_name": "fsm_12B",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "modeldoc": true,
            "portNumber": "2",
            "portType": "Inport",
            "project": "FSM",
            "tool": "Simulink",
            "variable_name": "apfail",
            "width": 1,
            "fretComponent": "FSM",
            "_id": "fsm_12B/apfail"
        },
        {
            "component_name": "fsm_12B",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "modeldoc": true,
            "portNumber": "4",
            "portType": "Inport",
            "project": "FSM",
            "tool": "Simulink",
            "variable_name": "limits",
            "width": 1,
            "fretComponent": "FSM",
            "_id": "fsm_12B/limits"
        },
        {
            "component_name": "fsm_12B",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "modeldoc": true,
            "portNumber": "1",
            "portType": "Inport",
            "project": "FSM",
            "tool": "Simulink",
            "variable_name": "standby",
            "width": 1,
            "fretComponent": "FSM",
            "_id": "fsm_12B/standby"
        },
        {
            "component_name": "fsm_12B",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "modeldoc": true,
            "portNumber": "3",
            "portType": "Inport",
            "project": "FSM",
            "tool": "Simulink",
            "variable_name": "supported",
            "width": 1,
            "fretComponent": "FSM",
            "_id": "fsm_12B/supported"
        },
        {
            "project": "Liquid_mixer",
            "modeldoc": true,
            "variable_name": "liquidlevel1",
            "portType": "Inport",
            "portNumber": "",
            "component_name": "liquidmixer",
            "tool": "Simulink",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "width": 1,
            "fretComponent": "liquid_mixer",
            "_id": "liquidlevel1"
        },
        {
            "project": "Liquid_mixer",
            "modeldoc": true,
            "variable_name": "liquidlevel2",
            "portType": "Inport",
            "portNumber": "",
            "component_name": "liquidmixer",
            "tool": "Simulink",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "width": 1,
            "fretComponent": "liquid_mixer",
            "_id": "liquidlevel2"
        },
        {
            "project": "Liquid_mixer",
            "modeldoc": true,
            "variable_name": "startbutton",
            "portType": "Inport",
            "portNumber": "",
            "component_name": "liquidmixer",
            "tool": "Simulink",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "width": 1,
            "fretComponent": "liquid_mixer",
            "_id": "startbutton"
        },
        {
            "project": "Liquid_mixer",
            "modeldoc": true,
            "variable_name": "stirringmotor",
            "portType": "Outport",
            "portNumber": "",
            "component_name": "liquidmixer",
            "tool": "Simulink",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "width": 1,
            "fretComponent": "liquid_mixer",
            "_id": "stirringmotor"
        },
        {
            "project": "Liquid_mixer",
            "modeldoc": true,
            "variable_name": "timer120secexpire",
            "portType": "Inport",
            "portNumber": "",
            "component_name": "liquidmixer",
            "tool": "Simulink",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "width": 1,
            "fretComponent": "liquid_mixer",
            "_id": "timer120secexpire"
        },
        {
            "project": "Liquid_mixer",
            "modeldoc": true,
            "variable_name": "timer120secstart",
            "portType": "Outport",
            "portNumber": "",
            "component_name": "liquidmixer",
            "tool": "Simulink",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "width": 1,
            "fretComponent": "liquid_mixer",
            "_id": "timer120secstart"
        },
        {
            "project": "Liquid_mixer",
            "modeldoc": true,
            "variable_name": "timer60secexpire",
            "portType": "Inport",
            "portNumber": "",
            "component_name": "liquidmixer",
            "tool": "Simulink",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "width": 1,
            "fretComponent": "liquid_mixer",
            "_id": "timer60secexpire"
        },
        {
            "project": "Liquid_mixer",
            "modeldoc": true,
            "variable_name": "timer60secstart",
            "portType": "Outport",
            "portNumber": "",
            "component_name": "liquidmixer",
            "tool": "Simulink",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "width": 1,
            "fretComponent": "liquid_mixer",
            "_id": "timer60secstart"
        },
        {
            "project": "Liquid_mixer",
            "modeldoc": true,
            "variable_name": "valve0",
            "portType": "Outport",
            "portNumber": "",
            "component_name": "liquidmixer",
            "tool": "Simulink",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "width": 1,
            "fretComponent": "liquid_mixer",
            "_id": "valve0"
        },
        {
            "project": "Liquid_mixer",
            "modeldoc": true,
            "variable_name": "valve1",
            "portType": "Outport",
            "portNumber": "",
            "component_name": "liquidmixer",
            "tool": "Simulink",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "width": 1,
            "fretComponent": "liquid_mixer",
            "_id": "valve1"
        },
        {
            "project": "Liquid_mixer",
            "modeldoc": true,
            "variable_name": "valve2",
            "portType": "Outport",
            "portNumber": "",
            "component_name": "liquidmixer",
            "tool": "Simulink",
            "dataType": [
                "boolean"
            ],
            "dimensions": [
                1,
                1
            ],
            "width": 1,
            "fretComponent": "liquid_mixer",
            "_id": "valve2"
        }
    ]
}