{
    "requirements": [
        {
            "reqid": "PWR-0100",
            "parent_reqid": "PWR-0000",
            "project": "PWR_Hybrid",
            "rationale": "",
            "comments": "",
            "fulltext": "If SCRAM DRC shall immediately satisfy !OP_MODE",
            "status": "",
            "semantics": {
                "type": "nasa",
                "scope": {
                    "type": "null"
                },
                "condition": "regular",
                "probability": "null",
                "timing": "immediately",
                "response": "satisfaction",
                "variables": [
                    "SCRAM",
                    "OP_MODE"
                ],
                "qualifier_word": "if",
                "pre_condition": "(SCRAM)",
                "regular_condition": "(SCRAM)",
                "conditionTextRange": [
                    0,
                    7
                ],
                "component_name": "DRC",
                "componentTextRange": [
                    9,
                    11
                ],
                "timingTextRange": [
                    19,
                    29
                ],
                "post_condition": "(! OP_MODE)",
                "responseTextRange": [
                    31,
                    46
                ],
                "diagramVariables": "TC = <b><i>(SCRAM)</i></b>, Response = <b><i>(! OP_MODE)</i></b>.",
                "description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: first point in the interval if <b><i>(SCRAM)</i></b> is true and any point in the interval where <b><i>(SCRAM)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, if trigger holds then <b><i>(! OP_MODE)</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 if <b><i>(SCRAM)</i></b> is true and any point in the interval where <b><i>(SCRAM)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, with probability >=1, if trigger holds then <b><i>(! OP_MODE)</i></b> also holds at the same time point.",
                "diagram": "_media/user-interface/examples/svgDiagrams/null_regular_immediately_satisfaction.svg",
                "scope_mode_pt": "BAD_PT",
                "scope_mode_ft": "BAD_FT",
                "regular_condition_unexp_pt": "SCRAM",
                "regular_condition_unexp_ft": "SCRAM",
                "regular_condition_unexp_pctl": "SCRAM",
                "regular_condition_SMV_pt": "SCRAM",
                "regular_condition_SMV_ft": "SCRAM",
                "regular_condition_MLTL_ft": "SCRAM",
                "regular_condition_PRISM_pctl": "SCRAM",
                "post_condition_unexp_pt": "(! OP_MODE)",
                "post_condition_unexp_ft": "(! OP_MODE)",
                "post_condition_unexp_pctl": "(! OP_MODE)",
                "post_condition_SMV_pt": "(! OP_MODE)",
                "post_condition_SMV_ft": "(! OP_MODE)",
                "post_condition_MLTL_ft": "(! OP_MODE)",
                "post_condition_PRISM_pctl": "(! OP_MODE)",
                "ft": "((LAST V (((! SCRAM) & ((! LAST) & (X SCRAM))) -> (X (! OP_MODE)))) & (SCRAM -> (! OP_MODE)))",
                "pt": "(H ((SCRAM & (Z (! SCRAM))) -> (! OP_MODE)))",
                "pctl": "P>=1[((G (((! SCRAM) & (X SCRAM)) => (X (P>=1[(! OP_MODE)])))) & (SCRAM => (P>=1[(! OP_MODE)])))]",
                "ptExpanded": "(H ((SCRAM & (Z (! SCRAM))) -> (! OP_MODE)))",
                "CoCoSpecCode": "H(((SCRAM and ZtoPre(not (SCRAM))) => not (OP_MODE)))",
                "ftExpanded": "((LAST V (((! SCRAM) & ((! LAST) & (X SCRAM))) -> (X (! OP_MODE)))) & (SCRAM -> (! OP_MODE)))",
                "pctlExpanded": "P>=1[((G (((! SCRAM) & (X SCRAM)) => (X (P>=1[(! OP_MODE)])))) & (SCRAM => (P>=1[(! OP_MODE)])))]",
                "ftInfAUExpanded": "((G (((! SCRAM) & (X SCRAM)) -> (X (! OP_MODE)))) & (SCRAM -> (! OP_MODE)))",
                "mltlExpanded": "((G[0,M] (((! p0) & (F[1,1] p0)) -> (F[1,1] p1))) & (p0 -> p1))",
                "WESTMapping": "p0: SCRAM<br/>p1: (! OP_MODE)",
                "R2U2Code": "((((! SCRAM) && (F[1,1] SCRAM)) -> (F[1,1] (! OP_MODE))) && (((TAU == 0) && SCRAM) -> (! OP_MODE)))",
                "component": "DRC"
            },
            "_id": "1af49c60-2f9f-11f1-bda7-b107d916a2e5"
        },
        {
            "reqid": "PWR-0202",
            "parent_reqid": "PWR-0201",
            "project": "PWR_Hybrid",
            "rationale": "this is the opposite of PWR-1001. If not in op mode, never be in heatup, load following.",
            "comments": "",
            "fulltext": "While !OP_MODE DRC shall always satisfy (Heatup | Load_Follow)",
            "status": "",
            "semantics": {
                "type": "nasa",
                "scope": {
                    "type": "in"
                },
                "condition": "null",
                "probability": "null",
                "timing": "always",
                "response": "satisfaction",
                "variables": [
                    "OP_MODE",
                    "Heatup",
                    "Load_Follow"
                ],
                "scope_mode": "(! OP_MODE)",
                "scopeTextRange": [
                    0,
                    13
                ],
                "component_name": "DRC",
                "componentTextRange": [
                    15,
                    17
                ],
                "timingTextRange": [
                    25,
                    30
                ],
                "post_condition": "(( Heatup | Load_Follow ))",
                "responseTextRange": [
                    32,
                    61
                ],
                "diagramVariables": "M = <b><i>(! OP_MODE)</i></b>, Response = <b><i>(( Heatup | Load_Follow ))</i></b>.",
                "description": "SCOPE: in every interval where <b><i>(! OP_MODE)</i></b> holds.<br>TRIGGER: first point in the interval.<br>REQUIRED BEHAVIOR: for every trigger, <b><i>(( Heatup | Load_Follow ))</i></b> must hold at all time points between (and including) the trigger and the end of the interval.",
                "probabilistic_description": "SCOPE: in every interval where <b><i>(! OP_MODE)</i></b> holds.<br>TRIGGER: first point in the interval.<br>REQUIRED BEHAVIOR: for every trigger, with probability >=1, <b><i>(( Heatup | Load_Follow ))</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/in_null_always_satisfaction.svg",
                "scope_mode_pt": "(! OP_MODE)",
                "scope_mode_ft": "(! OP_MODE)",
                "scope_mode_pctl": "(! OP_MODE)",
                "post_condition_unexp_pt": "(Heatup | Load_Follow)",
                "post_condition_unexp_ft": "(Heatup | Load_Follow)",
                "post_condition_unexp_pctl": "(Heatup | Load_Follow)",
                "post_condition_SMV_pt": "(Heatup | Load_Follow)",
                "post_condition_SMV_ft": "(Heatup | Load_Follow)",
                "post_condition_MLTL_ft": "(Heatup | Load_Follow)",
                "post_condition_PRISM_pctl": "(Heatup | Load_Follow)",
                "ft": "(LAST V ((! OP_MODE) -> (Heatup | Load_Follow)))",
                "pt": "(H ((! OP_MODE) -> (Heatup | Load_Follow)))",
                "pctl": "P>=1[((G ((! (Fin_(! OP_MODE) & (! LAST))) | (X (P>=1[(Lin_(! OP_MODE) R (Heatup | Load_Follow))])))) & ((! OP_MODE) => (Lin_(! OP_MODE) | (P>=1[(Lin_(! OP_MODE) R (Heatup | Load_Follow))]))))]",
                "ptExpanded": "(H ((! OP_MODE) -> (Heatup | Load_Follow)))",
                "CoCoSpecCode": "H((not (OP_MODE) => (Heatup or Load_Follow)))",
                "ftExpanded": "(LAST V ((! OP_MODE) -> (Heatup | Load_Follow)))",
                "pctlExpanded": "P>=1[((G ((! (((! (! OP_MODE)) & (X (! OP_MODE))) & (! false))) | (X (P>=1[(((! OP_MODE) & (X (! (! OP_MODE)))) R (Heatup | Load_Follow))])))) & ((! OP_MODE) => (((! OP_MODE) & (X (! (! OP_MODE)))) | (P>=1[(((! OP_MODE) & (X (! (! OP_MODE)))) R (Heatup | Load_Follow))]))))]",
                "ftInfAUExpanded": "(G ((! OP_MODE) -> (Heatup | Load_Follow)))",
                "mltlExpanded": "(G[0,M] (p0 -> p1))",
                "WESTMapping": "p0: (! OP_MODE)<br/>p1: (Heatup | Load_Follow)",
                "R2U2Code": "((! OP_MODE) -> (Heatup || Load_Follow))",
                "component": "DRC"
            },
            "_id": "29bfe300-31e1-11f1-820b-8f6ab14cd565"
        },
        {
            "reqid": "PWR-0201",
            "parent_reqid": "",
            "project": "PWR_Hybrid",
            "rationale": "When in operating mode, the DRC shall always be in heatup or load following mode, but not both at once. The DRC will also not be in cold shutdown or SCRAM.",
            "comments": "",
            "fulltext": "When OP_MODE DRC shall always satisfy (Heatup | Load_Follow) & !(!Heatup & !Load_Follow) & !(SCRAM | Cold_Shutdown)",
            "status": "",
            "semantics": {
                "type": "nasa",
                "scope": {
                    "type": "null"
                },
                "condition": "regular",
                "probability": "null",
                "timing": "always",
                "response": "satisfaction",
                "variables": [
                    "OP_MODE",
                    "Heatup",
                    "Load_Follow",
                    "SCRAM",
                    "Cold_Shutdown"
                ],
                "qualifier_word": "when",
                "pre_condition": "(OP_MODE)",
                "regular_condition": "(OP_MODE)",
                "conditionTextRange": [
                    0,
                    11
                ],
                "component_name": "DRC",
                "componentTextRange": [
                    13,
                    15
                ],
                "timingTextRange": [
                    23,
                    28
                ],
                "post_condition": "(( Heatup | Load_Follow ) & ! ( ! Heatup & ! Load_Follow ) & ! ( SCRAM | Cold_Shutdown ))",
                "responseTextRange": [
                    30,
                    114
                ],
                "diagramVariables": "TC = <b><i>(OP_MODE)</i></b>, Response = <b><i>(( Heatup | Load_Follow ) & ! ( ! Heatup & ! Load_Follow ) & ! ( SCRAM | Cold_Shutdown ))</i></b>.",
                "description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: first point in the interval if <b><i>(OP_MODE)</i></b> is true and any point in the interval where <b><i>(OP_MODE)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, <b><i>(( Heatup | Load_Follow ) & ! ( ! Heatup & ! Load_Follow ) & ! ( SCRAM | Cold_Shutdown ))</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 if <b><i>(OP_MODE)</i></b> is true and any point in the interval where <b><i>(OP_MODE)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, with probability >=1, <b><i>(( Heatup | Load_Follow ) & ! ( ! Heatup & ! Load_Follow ) & ! ( SCRAM | Cold_Shutdown ))</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_regular_always_satisfaction.svg",
                "scope_mode_pt": "BAD_PT",
                "scope_mode_ft": "BAD_FT",
                "regular_condition_unexp_pt": "OP_MODE",
                "regular_condition_unexp_ft": "OP_MODE",
                "regular_condition_unexp_pctl": "OP_MODE",
                "regular_condition_SMV_pt": "OP_MODE",
                "regular_condition_SMV_ft": "OP_MODE",
                "regular_condition_MLTL_ft": "OP_MODE",
                "regular_condition_PRISM_pctl": "OP_MODE",
                "post_condition_unexp_pt": "(((Heatup | Load_Follow) & (! ((! Heatup) & (! Load_Follow)))) & (! (SCRAM | Cold_Shutdown)))",
                "post_condition_unexp_ft": "(((Heatup | Load_Follow) & (! ((! Heatup) & (! Load_Follow)))) & (! (SCRAM | Cold_Shutdown)))",
                "post_condition_unexp_pctl": "(((Heatup | Load_Follow) & (! ((! Heatup) & (! Load_Follow)))) & (! (SCRAM | Cold_Shutdown)))",
                "post_condition_SMV_pt": "(((Heatup | Load_Follow) & (! ((! Heatup) & (! Load_Follow)))) & (! (SCRAM | Cold_Shutdown)))",
                "post_condition_SMV_ft": "(((Heatup | Load_Follow) & (! ((! Heatup) & (! Load_Follow)))) & (! (SCRAM | Cold_Shutdown)))",
                "post_condition_MLTL_ft": "(((Heatup | Load_Follow) & (! ((! Heatup) & (! Load_Follow)))) & (! (SCRAM | Cold_Shutdown)))",
                "post_condition_PRISM_pctl": "(((Heatup | Load_Follow) & (! ((! Heatup) & (! Load_Follow)))) & (! (SCRAM | Cold_Shutdown)))",
                "ft": "((LAST V (((! OP_MODE) & ((! LAST) & (X OP_MODE))) -> (X (LAST V (((Heatup | Load_Follow) & (! ((! Heatup) & (! Load_Follow)))) & (! (SCRAM | Cold_Shutdown))))))) & (OP_MODE -> (LAST V (((Heatup | Load_Follow) & (! ((! Heatup) & (! Load_Follow)))) & (! (SCRAM | Cold_Shutdown))))))",
                "pt": "(H ((H (! OP_MODE)) | (((Heatup | Load_Follow) & (! ((! Heatup) & (! Load_Follow)))) & (! (SCRAM | Cold_Shutdown)))))",
                "pctl": "P>=1[((G (((! OP_MODE) & (X OP_MODE)) => (X (P>=1[(G (((Heatup | Load_Follow) & (! ((! Heatup) & (! Load_Follow)))) & (! (SCRAM | Cold_Shutdown))))])))) & (OP_MODE => (P>=1[(G (((Heatup | Load_Follow) & (! ((! Heatup) & (! Load_Follow)))) & (! (SCRAM | Cold_Shutdown))))])))]",
                "ptExpanded": "(H ((H (! OP_MODE)) | ((Heatup | Load_Follow) & (! (SCRAM | Cold_Shutdown)))))",
                "CoCoSpecCode": "H((H(not (OP_MODE)) or ((Heatup or Load_Follow) and not ((SCRAM or Cold_Shutdown)))))",
                "ftExpanded": "((LAST V (((! OP_MODE) & ((! LAST) & (X OP_MODE))) -> (X (LAST V ((Heatup | Load_Follow) & (! (SCRAM | Cold_Shutdown))))))) & (OP_MODE -> (LAST V ((Heatup | Load_Follow) & (! (SCRAM | Cold_Shutdown))))))",
                "pctlExpanded": "P>=1[((G (((! OP_MODE) & (X OP_MODE)) => (X (P>=1[(G (((Heatup | Load_Follow) & (! ((! Heatup) & (! Load_Follow)))) & (! (SCRAM | Cold_Shutdown))))])))) & (OP_MODE => (P>=1[(G (((Heatup | Load_Follow) & (! ((! Heatup) & (! Load_Follow)))) & (! (SCRAM | Cold_Shutdown))))])))]",
                "ftInfAUExpanded": "((G (((! OP_MODE) & (X OP_MODE)) -> (X (G ((Heatup | Load_Follow) & (! (SCRAM | Cold_Shutdown))))))) & (OP_MODE -> (G ((Heatup | Load_Follow) & (! (SCRAM | Cold_Shutdown))))))",
                "mltlExpanded": "((G[0,M] (((! p0) & (F[1,1] p0)) -> (G[1,M] p1))) & (p0 -> (G[0,M] p1)))",
                "WESTMapping": "p0: OP_MODE<br/>p1: ((Heatup | Load_Follow) & (! (SCRAM | Cold_Shutdown)))",
                "R2U2Code": "((((! OP_MODE) && (F[1,1] OP_MODE)) -> (G[1,M] ((Heatup || Load_Follow) && (! (SCRAM || Cold_Shutdown))))) && (((TAU == 0) && OP_MODE) -> (G[0,M] ((Heatup || Load_Follow) && (! (SCRAM || Cold_Shutdown))))))",
                "component": "DRC"
            },
            "_id": "3a0697b0-2f91-11f1-bda7-b107d916a2e5"
        },
        {
            "reqid": "PWR-0200",
            "parent_reqid": "",
            "project": "PWR_Hybrid",
            "rationale": "",
            "comments": "",
            "fulltext": "While OP_MODE DRC shall always satisfy Heatup | Load_Follow",
            "status": "",
            "semantics": {
                "type": "nasa",
                "scope": {
                    "type": "in"
                },
                "condition": "null",
                "probability": "null",
                "timing": "always",
                "response": "satisfaction",
                "variables": [
                    "OP_MODE",
                    "Heatup",
                    "Load_Follow"
                ],
                "scope_mode": "(OP_MODE)",
                "scopeTextRange": [
                    0,
                    12
                ],
                "component_name": "DRC",
                "componentTextRange": [
                    14,
                    16
                ],
                "timingTextRange": [
                    24,
                    29
                ],
                "post_condition": "(Heatup | Load_Follow)",
                "responseTextRange": [
                    31,
                    58
                ],
                "diagramVariables": "M = <b><i>(OP_MODE)</i></b>, Response = <b><i>(Heatup | Load_Follow)</i></b>.",
                "description": "SCOPE: in every interval where <b><i>(OP_MODE)</i></b> holds.<br>TRIGGER: first point in the interval.<br>REQUIRED BEHAVIOR: for every trigger, <b><i>(Heatup | Load_Follow)</i></b> must hold at all time points between (and including) the trigger and the end of the interval.",
                "probabilistic_description": "SCOPE: in every interval where <b><i>(OP_MODE)</i></b> holds.<br>TRIGGER: first point in the interval.<br>REQUIRED BEHAVIOR: for every trigger, with probability >=1, <b><i>(Heatup | Load_Follow)</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/in_null_always_satisfaction.svg",
                "scope_mode_pt": "OP_MODE",
                "scope_mode_ft": "OP_MODE",
                "scope_mode_pctl": "OP_MODE",
                "post_condition_unexp_pt": "(Heatup | Load_Follow)",
                "post_condition_unexp_ft": "(Heatup | Load_Follow)",
                "post_condition_unexp_pctl": "(Heatup | Load_Follow)",
                "post_condition_SMV_pt": "(Heatup | Load_Follow)",
                "post_condition_SMV_ft": "(Heatup | Load_Follow)",
                "post_condition_MLTL_ft": "(Heatup | Load_Follow)",
                "post_condition_PRISM_pctl": "(Heatup | Load_Follow)",
                "ft": "(LAST V (OP_MODE -> (Heatup | Load_Follow)))",
                "pt": "(H (OP_MODE -> (Heatup | Load_Follow)))",
                "pctl": "P>=1[((G ((! (Fin_OP_MODE & (! LAST))) | (X (P>=1[(Lin_OP_MODE R (Heatup | Load_Follow))])))) & (OP_MODE => (Lin_OP_MODE | (P>=1[(Lin_OP_MODE R (Heatup | Load_Follow))]))))]",
                "ptExpanded": "(H (OP_MODE -> (Heatup | Load_Follow)))",
                "CoCoSpecCode": "H((OP_MODE => (Heatup or Load_Follow)))",
                "ftExpanded": "(LAST V (OP_MODE -> (Heatup | Load_Follow)))",
                "pctlExpanded": "P>=1[((G ((! (((! OP_MODE) & (X OP_MODE)) & (! false))) | (X (P>=1[((OP_MODE & (X (! OP_MODE))) R (Heatup | Load_Follow))])))) & (OP_MODE => ((OP_MODE & (X (! OP_MODE))) | (P>=1[((OP_MODE & (X (! OP_MODE))) R (Heatup | Load_Follow))]))))]",
                "ftInfAUExpanded": "(G (OP_MODE -> (Heatup | Load_Follow)))",
                "mltlExpanded": "(G[0,M] (p0 -> p1))",
                "WESTMapping": "p0: OP_MODE<br/>p1: (Heatup | Load_Follow)",
                "R2U2Code": "(OP_MODE -> (Heatup || Load_Follow))",
                "component": "DRC"
            },
            "_id": "50de1300-2fa0-11f1-b1b5-5117d78e7f0f"
        },
        {
            "reqid": "PWR-3002",
            "parent_reqid": "",
            "project": "PWR_Hybrid",
            "rationale": "The reactor will never be in heatup mode longer than a predetermined maximum heatup duration, or else it will trigger a scram.",
            "comments": "",
            "fulltext": "if t_max_exceeded DRC shall at the next timepoint satisfy SCRAM",
            "status": "",
            "semantics": {
                "type": "nasa",
                "scope": {
                    "type": "null"
                },
                "condition": "regular",
                "probability": "null",
                "timing": "next",
                "response": "satisfaction",
                "variables": [
                    "t_max_exceeded",
                    "SCRAM"
                ],
                "qualifier_word": "if",
                "pre_condition": "(t_max_exceeded)",
                "regular_condition": "(t_max_exceeded)",
                "conditionTextRange": [
                    0,
                    16
                ],
                "component_name": "DRC",
                "componentTextRange": [
                    18,
                    20
                ],
                "timingTextRange": [
                    28,
                    48
                ],
                "post_condition": "(SCRAM)",
                "responseTextRange": [
                    50,
                    62
                ],
                "diagramVariables": "TC = <b><i>(t_max_exceeded)</i></b>, Response = <b><i>(SCRAM)</i></b>.",
                "description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: first point in the interval if <b><i>(t_max_exceeded)</i></b> is true and any point in the interval where <b><i>(t_max_exceeded)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, <b><i>(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>(t_max_exceeded)</i></b> is true and any point in the interval where <b><i>(t_max_exceeded)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, with probability >=1, <b><i>(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": "t_max_exceeded",
                "regular_condition_unexp_ft": "t_max_exceeded",
                "regular_condition_unexp_pctl": "t_max_exceeded",
                "regular_condition_SMV_pt": "t_max_exceeded",
                "regular_condition_SMV_ft": "t_max_exceeded",
                "regular_condition_MLTL_ft": "t_max_exceeded",
                "regular_condition_PRISM_pctl": "t_max_exceeded",
                "post_condition_unexp_pt": "SCRAM",
                "post_condition_unexp_ft": "SCRAM",
                "post_condition_unexp_pctl": "SCRAM",
                "post_condition_SMV_pt": "SCRAM",
                "post_condition_SMV_ft": "SCRAM",
                "post_condition_MLTL_ft": "SCRAM",
                "post_condition_PRISM_pctl": "SCRAM",
                "ft": "((LAST V (((! t_max_exceeded) & ((! LAST) & (X t_max_exceeded))) -> (X (LAST | (X SCRAM))))) & (t_max_exceeded -> (LAST | (X SCRAM))))",
                "pt": "(H ((Y (t_max_exceeded & (Z (! t_max_exceeded)))) -> (SCRAM | (Z FALSE))))",
                "pctl": "P>=1[((G (((! t_max_exceeded) & (X t_max_exceeded)) => (X (P>=1[(LAST | (X SCRAM))])))) & (t_max_exceeded => (P>=1[(LAST | (X SCRAM))])))]",
                "ptExpanded": "(H ((Y (t_max_exceeded & (Z (! t_max_exceeded)))) -> (SCRAM | (Z FALSE))))",
                "CoCoSpecCode": "H((YtoPre((t_max_exceeded and ZtoPre(not (t_max_exceeded)))) => (SCRAM or ZtoPre(false))))",
                "ftExpanded": "((LAST V (((! t_max_exceeded) & ((! LAST) & (X t_max_exceeded))) -> (X (LAST | (X SCRAM))))) & (t_max_exceeded -> (LAST | (X SCRAM))))",
                "pctlExpanded": "P>=1[((G (((! t_max_exceeded) & (X t_max_exceeded)) => (X (P>=1[(false | (X SCRAM))])))) & (t_max_exceeded => (P>=1[(false | (X SCRAM))])))]",
                "ftInfAUExpanded": "((G (((! t_max_exceeded) & (X t_max_exceeded)) -> (X (X SCRAM)))) & (t_max_exceeded -> (X SCRAM)))",
                "mltlExpanded": "((G[0,M] (((! p0) & (F[1,1] p0)) -> (F[2,2] p1))) & (p0 -> (F[1,1] p1)))",
                "WESTMapping": "p0: t_max_exceeded<br/>p1: SCRAM",
                "R2U2Code": "((((! t_max_exceeded) && (F[1,1] t_max_exceeded)) -> (F[2,2] SCRAM)) && (((TAU == 0) && t_max_exceeded) -> (F[1,1] SCRAM)))",
                "component": "DRC"
            },
            "_id": "96d7c900-2f96-11f1-bda7-b107d916a2e5"
        },
        {
            "reqid": "PWR-3001",
            "parent_reqid": "",
            "project": "PWR_Hybrid",
            "rationale": "While in heatup mode, the reactor will trip if the rate of average temperature change is above a certain threshold. ",
            "comments": "",
            "fulltext": "While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM",
            "status": "",
            "semantics": {
                "type": "nasa",
                "scope": {
                    "type": "in"
                },
                "condition": "regular",
                "probability": "null",
                "timing": "next",
                "response": "satisfaction",
                "variables": [
                    "Heatup",
                    "t_dot_exceeded",
                    "SCRAM"
                ],
                "scope_mode": "(Heatup)",
                "scopeTextRange": [
                    0,
                    11
                ],
                "qualifier_word": "if",
                "pre_condition": "(t_dot_exceeded)",
                "regular_condition": "(t_dot_exceeded)",
                "conditionTextRange": [
                    13,
                    29
                ],
                "component_name": "DRC",
                "componentTextRange": [
                    31,
                    33
                ],
                "timingTextRange": [
                    41,
                    61
                ],
                "post_condition": "(SCRAM)",
                "responseTextRange": [
                    63,
                    75
                ],
                "diagramVariables": "M = <b><i>(Heatup)</i></b>, TC = <b><i>(t_dot_exceeded)</i></b>, Response = <b><i>(SCRAM)</i></b>.",
                "description": "SCOPE: in every interval where <b><i>(Heatup)</i></b> holds.<br>TRIGGER: first point in the interval if <b><i>(t_dot_exceeded)</i></b> is true and any point in the interval where <b><i>(t_dot_exceeded)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, <b><i>(SCRAM)</i></b> must hold at the next time step.",
                "probabilistic_description": "SCOPE: in every interval where <b><i>(Heatup)</i></b> holds.<br>TRIGGER: first point in the interval if <b><i>(t_dot_exceeded)</i></b> is true and any point in the interval where <b><i>(t_dot_exceeded)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, with probability >=1, <b><i>(SCRAM)</i></b> must hold at the next time step.",
                "diagram": "_media/user-interface/examples/svgDiagrams/in_regular_next_satisfaction.svg",
                "scope_mode_pt": "Heatup",
                "scope_mode_ft": "Heatup",
                "scope_mode_pctl": "Heatup",
                "regular_condition_unexp_pt": "t_dot_exceeded",
                "regular_condition_unexp_ft": "t_dot_exceeded",
                "regular_condition_unexp_pctl": "t_dot_exceeded",
                "regular_condition_SMV_pt": "t_dot_exceeded",
                "regular_condition_SMV_ft": "t_dot_exceeded",
                "regular_condition_MLTL_ft": "t_dot_exceeded",
                "regular_condition_PRISM_pctl": "t_dot_exceeded",
                "post_condition_unexp_pt": "SCRAM",
                "post_condition_unexp_ft": "SCRAM",
                "post_condition_unexp_pctl": "SCRAM",
                "post_condition_SMV_pt": "SCRAM",
                "post_condition_SMV_ft": "SCRAM",
                "post_condition_MLTL_ft": "SCRAM",
                "post_condition_PRISM_pctl": "SCRAM",
                "ft": "((LAST V ((! (Fin_Heatup & (! LAST))) | (X (((Lin_Heatup | LAST) V (((! t_dot_exceeded) & ((! LAST) & ((X t_dot_exceeded) & (! (Lin_Heatup | LAST))))) -> ((X ((Lin_Heatup | LAST) | (X SCRAM))) & (! (Lin_Heatup | LAST))))) & (t_dot_exceeded -> ((Lin_Heatup | LAST) | (X SCRAM))))))) & (Heatup -> (((Lin_Heatup | LAST) V (((! t_dot_exceeded) & ((! LAST) & ((X t_dot_exceeded) & (! (Lin_Heatup | LAST))))) -> ((X ((Lin_Heatup | LAST) | (X SCRAM))) & (! (Lin_Heatup | LAST))))) & (t_dot_exceeded -> ((Lin_Heatup | LAST) | (X SCRAM))))))",
                "pt": "((H (Lin_Heatup -> (Y (((Y (t_dot_exceeded & ((Y (! t_dot_exceeded)) | Fin_Heatup))) -> (SCRAM | Fin_Heatup)) S (((Y (t_dot_exceeded & ((Y (! t_dot_exceeded)) | Fin_Heatup))) -> (SCRAM | Fin_Heatup)) & Fin_Heatup))))) & (((! Lin_Heatup) S ((! Lin_Heatup) & Fin_Heatup)) -> (((Y (t_dot_exceeded & ((Y (! t_dot_exceeded)) | Fin_Heatup))) -> (SCRAM | Fin_Heatup)) S (((Y (t_dot_exceeded & ((Y (! t_dot_exceeded)) | Fin_Heatup))) -> (SCRAM | Fin_Heatup)) & Fin_Heatup))))",
                "pctl": "P>=1[((G ((! (Fin_Heatup & (! LAST))) | (X ((Lin_Heatup R (((! t_dot_exceeded) & ((X t_dot_exceeded) & (! Lin_Heatup))) => ((X (P>=1[(Lin_Heatup | ((X SCRAM) & (! Lin_Heatup)))])) & (! Lin_Heatup)))) & (t_dot_exceeded => (P>=1[(Lin_Heatup | ((X SCRAM) & (! Lin_Heatup)))])))))) & (Heatup => (Lin_Heatup | ((Lin_Heatup R (((! t_dot_exceeded) & ((X t_dot_exceeded) & (! Lin_Heatup))) => ((X (P>=1[(Lin_Heatup | ((X SCRAM) & (! Lin_Heatup)))])) & (! Lin_Heatup)))) & (t_dot_exceeded => (P>=1[(Lin_Heatup | ((X SCRAM) & (! Lin_Heatup)))]))))))]",
                "ptExpanded": "((H (((! Heatup) & (Y Heatup)) -> (Y (((Y (t_dot_exceeded & ((Y (! t_dot_exceeded)) | (Heatup & (Z (! Heatup)))))) -> (SCRAM | (Heatup & (Z (! Heatup))))) S (((Y (t_dot_exceeded & ((Y (! t_dot_exceeded)) | (Heatup & (Z (! Heatup)))))) -> (SCRAM | (Heatup & (Z (! Heatup))))) & (Heatup & (Z (! Heatup)))))))) & (((! ((! Heatup) & (Y Heatup))) S ((! ((! Heatup) & (Y Heatup))) & (Heatup & (Z (! Heatup))))) -> (((Y (t_dot_exceeded & ((Y (! t_dot_exceeded)) | (Heatup & (Z (! Heatup)))))) -> (SCRAM | (Heatup & (Z (! Heatup))))) S (((Y (t_dot_exceeded & ((Y (! t_dot_exceeded)) | (Heatup & (Z (! Heatup)))))) -> (SCRAM | (Heatup & (Z (! Heatup))))) & (Heatup & (Z (! Heatup)))))))",
                "CoCoSpecCode": "(H(((not (Heatup) and YtoPre(Heatup)) => YtoPre(SI((Heatup and ZtoPre(not (Heatup))),(YtoPre((t_dot_exceeded and (YtoPre(not (t_dot_exceeded)) or (Heatup and ZtoPre(not (Heatup)))))) => (SCRAM or (Heatup and ZtoPre(not (Heatup))))))))) and (SI((Heatup and ZtoPre(not (Heatup))),not ((not (Heatup) and YtoPre(Heatup)))) => SI((Heatup and ZtoPre(not (Heatup))),(YtoPre((t_dot_exceeded and (YtoPre(not (t_dot_exceeded)) or (Heatup and ZtoPre(not (Heatup)))))) => (SCRAM or (Heatup and ZtoPre(not (Heatup))))))))",
                "ftExpanded": "((LAST V ((! ((((! Heatup) & (! LAST)) & (X Heatup)) & (! LAST))) | (X (((((Heatup & (! LAST)) & (X (! Heatup))) | LAST) V (((! t_dot_exceeded) & ((! LAST) & ((X t_dot_exceeded) & (! (((Heatup & (! LAST)) & (X (! Heatup))) | LAST))))) -> ((X ((((Heatup & (! LAST)) & (X (! Heatup))) | LAST) | (X SCRAM))) & (! (((Heatup & (! LAST)) & (X (! Heatup))) | LAST))))) & (t_dot_exceeded -> ((((Heatup & (! LAST)) & (X (! Heatup))) | LAST) | (X SCRAM))))))) & (Heatup -> (((((Heatup & (! LAST)) & (X (! Heatup))) | LAST) V (((! t_dot_exceeded) & ((! LAST) & ((X t_dot_exceeded) & (! (((Heatup & (! LAST)) & (X (! Heatup))) | LAST))))) -> ((X ((((Heatup & (! LAST)) & (X (! Heatup))) | LAST) | (X SCRAM))) & (! (((Heatup & (! LAST)) & (X (! Heatup))) | LAST))))) & (t_dot_exceeded -> ((((Heatup & (! LAST)) & (X (! Heatup))) | LAST) | (X SCRAM))))))",
                "pctlExpanded": "P>=1[((G ((! (((! Heatup) & (X Heatup)) & (! false))) | (X (((Heatup & (X (! Heatup))) R (((! t_dot_exceeded) & ((X t_dot_exceeded) & (! (Heatup & (X (! Heatup)))))) => ((X (P>=1[((Heatup & (X (! Heatup))) | ((X SCRAM) & (! (Heatup & (X (! Heatup))))))])) & (! (Heatup & (X (! Heatup))))))) & (t_dot_exceeded => (P>=1[((Heatup & (X (! Heatup))) | ((X SCRAM) & (! (Heatup & (X (! Heatup))))))])))))) & (Heatup => ((Heatup & (X (! Heatup))) | (((Heatup & (X (! Heatup))) R (((! t_dot_exceeded) & ((X t_dot_exceeded) & (! (Heatup & (X (! Heatup)))))) => ((X (P>=1[((Heatup & (X (! Heatup))) | ((X SCRAM) & (! (Heatup & (X (! Heatup))))))])) & (! (Heatup & (X (! Heatup))))))) & (t_dot_exceeded => (P>=1[((Heatup & (X (! Heatup))) | ((X SCRAM) & (! (Heatup & (X (! Heatup))))))]))))))]",
                "ftInfAUExpanded": "((G ((! ((! Heatup) & (X Heatup))) | (X (((Heatup & (X (! Heatup))) V (((! t_dot_exceeded) & ((X t_dot_exceeded) & (! (Heatup & (X (! Heatup)))))) -> ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & (! (Heatup & (X (! Heatup))))))) & (t_dot_exceeded -> ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & (Heatup -> (((Heatup & (X (! Heatup))) V (((! t_dot_exceeded) & ((X t_dot_exceeded) & (! (Heatup & (X (! Heatup)))))) -> ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & (! (Heatup & (X (! Heatup))))))) & (t_dot_exceeded -> ((Heatup & (X (! Heatup))) | (X SCRAM))))))",
                "mltlExpanded": "((G[0,M] (((p0 & ((! p1) & ((F[1,1] p1) & (F[1,1] p0)))) -> ((F[2,2] (! p0)) | (F[2,2] p2))) & (((! p0) & (F[1,1] p0)) -> (F[1,1] (p1 -> ((F[1,1] (! p0)) | (F[1,1] p2))))))) & ((p0 & p1) -> ((F[1,1] (! p0)) | (F[1,1] p2))))",
                "WESTMapping": "p0: Heatup<br/>p1: t_dot_exceeded<br/>p2: SCRAM",
                "R2U2Code": "((((Heatup && ((! t_dot_exceeded) && ((F[1,1] t_dot_exceeded) && (F[1,1] Heatup)))) -> ((F[2,2] (! Heatup)) || (F[2,2] SCRAM))) && (((! Heatup) && (F[1,1] Heatup)) -> (F[1,1] (t_dot_exceeded -> ((F[1,1] (! Heatup)) || (F[1,1] SCRAM)))))) && (((TAU == 0) && (Heatup && t_dot_exceeded)) -> ((F[1,1] (! Heatup)) || (F[1,1] SCRAM))))",
                "component": "DRC"
            },
            "_id": "a6665110-2f92-11f1-bda7-b107d916a2e5"
        },
        {
            "reqid": "PWR-2001",
            "parent_reqid": "",
            "project": "PWR_Hybrid",
            "rationale": "When the reactor is in cold shutdown, it will only enter op mode (and heatup), when the STARTUP command is initiated. ",
            "comments": "",
            "fulltext": "While !SCRAM If Cold_Shutdown & STARTUP DRC shall at the next timepoint satisfy OP_MODE & Heatup",
            "status": "",
            "semantics": {
                "type": "nasa",
                "scope": {
                    "type": "in"
                },
                "condition": "regular",
                "probability": "null",
                "timing": "next",
                "response": "satisfaction",
                "variables": [
                    "SCRAM",
                    "Cold_Shutdown",
                    "STARTUP",
                    "OP_MODE",
                    "Heatup"
                ],
                "scope_mode": "(! SCRAM)",
                "scopeTextRange": [
                    0,
                    11
                ],
                "qualifier_word": "if",
                "pre_condition": "(Cold_Shutdown & STARTUP)",
                "regular_condition": "(Cold_Shutdown & STARTUP)",
                "conditionTextRange": [
                    13,
                    38
                ],
                "component_name": "DRC",
                "componentTextRange": [
                    40,
                    42
                ],
                "timingTextRange": [
                    50,
                    70
                ],
                "post_condition": "(OP_MODE & Heatup)",
                "responseTextRange": [
                    72,
                    95
                ],
                "diagramVariables": "M = <b><i>(! SCRAM)</i></b>, TC = <b><i>(Cold_Shutdown & STARTUP)</i></b>, Response = <b><i>(OP_MODE & Heatup)</i></b>.",
                "description": "SCOPE: in every interval where <b><i>(! SCRAM)</i></b> holds.<br>TRIGGER: first point in the interval if <b><i>(Cold_Shutdown & STARTUP)</i></b> is true and any point in the interval where <b><i>(Cold_Shutdown & STARTUP)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, <b><i>(OP_MODE & Heatup)</i></b> must hold at the next time step.",
                "probabilistic_description": "SCOPE: in every interval where <b><i>(! SCRAM)</i></b> holds.<br>TRIGGER: first point in the interval if <b><i>(Cold_Shutdown & STARTUP)</i></b> is true and any point in the interval where <b><i>(Cold_Shutdown & STARTUP)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, with probability >=1, <b><i>(OP_MODE & Heatup)</i></b> must hold at the next time step.",
                "diagram": "_media/user-interface/examples/svgDiagrams/in_regular_next_satisfaction.svg",
                "scope_mode_pt": "(! SCRAM)",
                "scope_mode_ft": "(! SCRAM)",
                "scope_mode_pctl": "(! SCRAM)",
                "regular_condition_unexp_pt": "(Cold_Shutdown & STARTUP)",
                "regular_condition_unexp_ft": "(Cold_Shutdown & STARTUP)",
                "regular_condition_unexp_pctl": "(Cold_Shutdown & STARTUP)",
                "regular_condition_SMV_pt": "(Cold_Shutdown & STARTUP)",
                "regular_condition_SMV_ft": "(Cold_Shutdown & STARTUP)",
                "regular_condition_MLTL_ft": "(Cold_Shutdown & STARTUP)",
                "regular_condition_PRISM_pctl": "(Cold_Shutdown & STARTUP)",
                "post_condition_unexp_pt": "(OP_MODE & Heatup)",
                "post_condition_unexp_ft": "(OP_MODE & Heatup)",
                "post_condition_unexp_pctl": "(OP_MODE & Heatup)",
                "post_condition_SMV_pt": "(OP_MODE & Heatup)",
                "post_condition_SMV_ft": "(OP_MODE & Heatup)",
                "post_condition_MLTL_ft": "(OP_MODE & Heatup)",
                "post_condition_PRISM_pctl": "(OP_MODE & Heatup)",
                "ft": "((LAST V ((! (Fin_(! SCRAM) & (! LAST))) | (X (((Lin_(! SCRAM) | LAST) V (((! (Cold_Shutdown & STARTUP)) & ((! LAST) & ((X (Cold_Shutdown & STARTUP)) & (! (Lin_(! SCRAM) | LAST))))) -> ((X ((Lin_(! SCRAM) | LAST) | (X (OP_MODE & Heatup)))) & (! (Lin_(! SCRAM) | LAST))))) & ((Cold_Shutdown & STARTUP) -> ((Lin_(! SCRAM) | LAST) | (X (OP_MODE & Heatup)))))))) & ((! SCRAM) -> (((Lin_(! SCRAM) | LAST) V (((! (Cold_Shutdown & STARTUP)) & ((! LAST) & ((X (Cold_Shutdown & STARTUP)) & (! (Lin_(! SCRAM) | LAST))))) -> ((X ((Lin_(! SCRAM) | LAST) | (X (OP_MODE & Heatup)))) & (! (Lin_(! SCRAM) | LAST))))) & ((Cold_Shutdown & STARTUP) -> ((Lin_(! SCRAM) | LAST) | (X (OP_MODE & Heatup)))))))",
                "pt": "((H (Lin_(! SCRAM) -> (Y (((Y ((Cold_Shutdown & STARTUP) & ((Y (! (Cold_Shutdown & STARTUP))) | Fin_(! SCRAM)))) -> ((OP_MODE & Heatup) | Fin_(! SCRAM))) S (((Y ((Cold_Shutdown & STARTUP) & ((Y (! (Cold_Shutdown & STARTUP))) | Fin_(! SCRAM)))) -> ((OP_MODE & Heatup) | Fin_(! SCRAM))) & Fin_(! SCRAM)))))) & (((! Lin_(! SCRAM)) S ((! Lin_(! SCRAM)) & Fin_(! SCRAM))) -> (((Y ((Cold_Shutdown & STARTUP) & ((Y (! (Cold_Shutdown & STARTUP))) | Fin_(! SCRAM)))) -> ((OP_MODE & Heatup) | Fin_(! SCRAM))) S (((Y ((Cold_Shutdown & STARTUP) & ((Y (! (Cold_Shutdown & STARTUP))) | Fin_(! SCRAM)))) -> ((OP_MODE & Heatup) | Fin_(! SCRAM))) & Fin_(! SCRAM)))))",
                "pctl": "P>=1[((G ((! (Fin_(! SCRAM) & (! LAST))) | (X ((Lin_(! SCRAM) R (((! (Cold_Shutdown & STARTUP)) & ((X (Cold_Shutdown & STARTUP)) & (! Lin_(! SCRAM)))) => ((X (P>=1[(Lin_(! SCRAM) | ((X (OP_MODE & Heatup)) & (! Lin_(! SCRAM))))])) & (! Lin_(! SCRAM))))) & ((Cold_Shutdown & STARTUP) => (P>=1[(Lin_(! SCRAM) | ((X (OP_MODE & Heatup)) & (! Lin_(! SCRAM))))])))))) & ((! SCRAM) => (Lin_(! SCRAM) | ((Lin_(! SCRAM) R (((! (Cold_Shutdown & STARTUP)) & ((X (Cold_Shutdown & STARTUP)) & (! Lin_(! SCRAM)))) => ((X (P>=1[(Lin_(! SCRAM) | ((X (OP_MODE & Heatup)) & (! Lin_(! SCRAM))))])) & (! Lin_(! SCRAM))))) & ((Cold_Shutdown & STARTUP) => (P>=1[(Lin_(! SCRAM) | ((X (OP_MODE & Heatup)) & (! Lin_(! SCRAM))))]))))))]",
                "ptExpanded": "((H ((SCRAM & (Y (! SCRAM))) -> (Y (((Y ((Cold_Shutdown & STARTUP) & ((Y (! (Cold_Shutdown & STARTUP))) | ((! SCRAM) & (Z SCRAM))))) -> ((OP_MODE & Heatup) | ((! SCRAM) & (Z SCRAM)))) S (((Y ((Cold_Shutdown & STARTUP) & ((Y (! (Cold_Shutdown & STARTUP))) | ((! SCRAM) & (Z SCRAM))))) -> ((OP_MODE & Heatup) | ((! SCRAM) & (Z SCRAM)))) & ((! SCRAM) & (Z SCRAM))))))) & (((! (SCRAM & (Y (! SCRAM)))) S ((! (SCRAM & (Y (! SCRAM)))) & ((! SCRAM) & (Z SCRAM)))) -> (((Y ((Cold_Shutdown & STARTUP) & ((Y (! (Cold_Shutdown & STARTUP))) | ((! SCRAM) & (Z SCRAM))))) -> ((OP_MODE & Heatup) | ((! SCRAM) & (Z SCRAM)))) S (((Y ((Cold_Shutdown & STARTUP) & ((Y (! (Cold_Shutdown & STARTUP))) | ((! SCRAM) & (Z SCRAM))))) -> ((OP_MODE & Heatup) | ((! SCRAM) & (Z SCRAM)))) & ((! SCRAM) & (Z SCRAM))))))",
                "CoCoSpecCode": "(H(((SCRAM and YtoPre(not (SCRAM))) => YtoPre(SI((not (SCRAM) and ZtoPre(SCRAM)),(YtoPre(((Cold_Shutdown and STARTUP) and (YtoPre(not ((Cold_Shutdown and STARTUP))) or (not (SCRAM) and ZtoPre(SCRAM))))) => ((OP_MODE and Heatup) or (not (SCRAM) and ZtoPre(SCRAM)))))))) and (SI((not (SCRAM) and ZtoPre(SCRAM)),not ((SCRAM and YtoPre(not (SCRAM))))) => SI((not (SCRAM) and ZtoPre(SCRAM)),(YtoPre(((Cold_Shutdown and STARTUP) and (YtoPre(not ((Cold_Shutdown and STARTUP))) or (not (SCRAM) and ZtoPre(SCRAM))))) => ((OP_MODE and Heatup) or (not (SCRAM) and ZtoPre(SCRAM)))))))",
                "ftExpanded": "((LAST V ((! (((SCRAM & (! LAST)) & (X (! SCRAM))) & (! LAST))) | (X ((((((! SCRAM) & (! LAST)) & (X SCRAM)) | LAST) V (((! (Cold_Shutdown & STARTUP)) & ((! LAST) & ((X (Cold_Shutdown & STARTUP)) & (! ((((! SCRAM) & (! LAST)) & (X SCRAM)) | LAST))))) -> ((X (((((! SCRAM) & (! LAST)) & (X SCRAM)) | LAST) | (X (OP_MODE & Heatup)))) & (! ((((! SCRAM) & (! LAST)) & (X SCRAM)) | LAST))))) & ((Cold_Shutdown & STARTUP) -> (((((! SCRAM) & (! LAST)) & (X SCRAM)) | LAST) | (X (OP_MODE & Heatup)))))))) & ((! SCRAM) -> ((((((! SCRAM) & (! LAST)) & (X SCRAM)) | LAST) V (((! (Cold_Shutdown & STARTUP)) & ((! LAST) & ((X (Cold_Shutdown & STARTUP)) & (! ((((! SCRAM) & (! LAST)) & (X SCRAM)) | LAST))))) -> ((X (((((! SCRAM) & (! LAST)) & (X SCRAM)) | LAST) | (X (OP_MODE & Heatup)))) & (! ((((! SCRAM) & (! LAST)) & (X SCRAM)) | LAST))))) & ((Cold_Shutdown & STARTUP) -> (((((! SCRAM) & (! LAST)) & (X SCRAM)) | LAST) | (X (OP_MODE & Heatup)))))))",
                "pctlExpanded": "P>=1[((G ((! (((! (! SCRAM)) & (X (! SCRAM))) & (! false))) | (X ((((! SCRAM) & (X (! (! SCRAM)))) R (((! (Cold_Shutdown & STARTUP)) & ((X (Cold_Shutdown & STARTUP)) & (! ((! SCRAM) & (X (! (! SCRAM))))))) => ((X (P>=1[(((! SCRAM) & (X (! (! SCRAM)))) | ((X (OP_MODE & Heatup)) & (! ((! SCRAM) & (X (! (! SCRAM)))))))])) & (! ((! SCRAM) & (X (! (! SCRAM)))))))) & ((Cold_Shutdown & STARTUP) => (P>=1[(((! SCRAM) & (X (! (! SCRAM)))) | ((X (OP_MODE & Heatup)) & (! ((! SCRAM) & (X (! (! SCRAM)))))))])))))) & ((! SCRAM) => (((! SCRAM) & (X (! (! SCRAM)))) | ((((! SCRAM) & (X (! (! SCRAM)))) R (((! (Cold_Shutdown & STARTUP)) & ((X (Cold_Shutdown & STARTUP)) & (! ((! SCRAM) & (X (! (! SCRAM))))))) => ((X (P>=1[(((! SCRAM) & (X (! (! SCRAM)))) | ((X (OP_MODE & Heatup)) & (! ((! SCRAM) & (X (! (! SCRAM)))))))])) & (! ((! SCRAM) & (X (! (! SCRAM)))))))) & ((Cold_Shutdown & STARTUP) => (P>=1[(((! SCRAM) & (X (! (! SCRAM)))) | ((X (OP_MODE & Heatup)) & (! ((! SCRAM) & (X (! (! SCRAM)))))))]))))))]",
                "ftInfAUExpanded": "((G ((! (SCRAM & (X (! SCRAM)))) | (X ((((! SCRAM) & (X SCRAM)) V (((! (Cold_Shutdown & STARTUP)) & ((X (Cold_Shutdown & STARTUP)) & (! ((! SCRAM) & (X SCRAM))))) -> ((X (((! SCRAM) & (X SCRAM)) | (X (OP_MODE & Heatup)))) & (! ((! SCRAM) & (X SCRAM)))))) & ((Cold_Shutdown & STARTUP) -> (((! SCRAM) & (X SCRAM)) | (X (OP_MODE & Heatup)))))))) & ((! SCRAM) -> ((((! SCRAM) & (X SCRAM)) V (((! (Cold_Shutdown & STARTUP)) & ((X (Cold_Shutdown & STARTUP)) & (! ((! SCRAM) & (X SCRAM))))) -> ((X (((! SCRAM) & (X SCRAM)) | (X (OP_MODE & Heatup)))) & (! ((! SCRAM) & (X SCRAM)))))) & ((Cold_Shutdown & STARTUP) -> (((! SCRAM) & (X SCRAM)) | (X (OP_MODE & Heatup)))))))",
                "mltlExpanded": "((G[0,M] (((p0 & ((! p1) & ((F[1,1] p1) & (F[1,1] p0)))) -> ((F[2,2] (! p0)) | (F[2,2] p2))) & (((! p0) & (F[1,1] p0)) -> (F[1,1] (p1 -> ((F[1,1] (! p0)) | (F[1,1] p2))))))) & ((p0 & p1) -> ((F[1,1] (! p0)) | (F[1,1] p2))))",
                "WESTMapping": "p0: (! SCRAM)<br/>p1: (Cold_Shutdown & STARTUP)<br/>p2: (OP_MODE & Heatup)",
                "R2U2Code": "(((((! SCRAM) && ((! (Cold_Shutdown && STARTUP)) && ((F[1,1] (Cold_Shutdown && STARTUP)) && (F[1,1] (! SCRAM))))) -> ((F[2,2] SCRAM) || (F[2,2] (OP_MODE && Heatup)))) && ((SCRAM && (F[1,1] (! SCRAM))) -> (F[1,1] ((Cold_Shutdown && STARTUP) -> ((F[1,1] SCRAM) || (F[1,1] (OP_MODE && Heatup))))))) && (((TAU == 0) && ((! SCRAM) && (Cold_Shutdown && STARTUP))) -> ((F[1,1] SCRAM) || (F[1,1] (OP_MODE && Heatup)))))",
                "component": "DRC"
            },
            "_id": "bfa3ea30-2f91-11f1-bda7-b107d916a2e5"
        },
        {
            "reqid": "PWR-3003",
            "parent_reqid": "",
            "project": "PWR_Hybrid",
            "rationale": "While in heatup mode, when the reactor reaches the minimum operating temperature, it will transition into load following mode.",
            "comments": "",
            "fulltext": "While Heatup if t_power_min DRC shall at the next timepoint satisfy (Load_Follow & !Heatup)",
            "status": "",
            "semantics": {
                "type": "nasa",
                "scope": {
                    "type": "in"
                },
                "condition": "regular",
                "probability": "null",
                "timing": "next",
                "response": "satisfaction",
                "variables": [
                    "Heatup",
                    "t_power_min",
                    "Load_Follow"
                ],
                "scope_mode": "(Heatup)",
                "scopeTextRange": [
                    0,
                    11
                ],
                "qualifier_word": "if",
                "pre_condition": "(t_power_min)",
                "regular_condition": "(t_power_min)",
                "conditionTextRange": [
                    13,
                    26
                ],
                "component_name": "DRC",
                "componentTextRange": [
                    28,
                    30
                ],
                "timingTextRange": [
                    38,
                    58
                ],
                "post_condition": "(( Load_Follow & ! Heatup ))",
                "responseTextRange": [
                    60,
                    90
                ],
                "diagramVariables": "M = <b><i>(Heatup)</i></b>, TC = <b><i>(t_power_min)</i></b>, Response = <b><i>(( Load_Follow & ! Heatup ))</i></b>.",
                "description": "SCOPE: in every interval where <b><i>(Heatup)</i></b> holds.<br>TRIGGER: first point in the interval if <b><i>(t_power_min)</i></b> is true and any point in the interval where <b><i>(t_power_min)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, <b><i>(( Load_Follow & ! Heatup ))</i></b> must hold at the next time step.",
                "probabilistic_description": "SCOPE: in every interval where <b><i>(Heatup)</i></b> holds.<br>TRIGGER: first point in the interval if <b><i>(t_power_min)</i></b> is true and any point in the interval where <b><i>(t_power_min)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, with probability >=1, <b><i>(( Load_Follow & ! Heatup ))</i></b> must hold at the next time step.",
                "diagram": "_media/user-interface/examples/svgDiagrams/in_regular_next_satisfaction.svg",
                "scope_mode_pt": "Heatup",
                "scope_mode_ft": "Heatup",
                "scope_mode_pctl": "Heatup",
                "regular_condition_unexp_pt": "t_power_min",
                "regular_condition_unexp_ft": "t_power_min",
                "regular_condition_unexp_pctl": "t_power_min",
                "regular_condition_SMV_pt": "t_power_min",
                "regular_condition_SMV_ft": "t_power_min",
                "regular_condition_MLTL_ft": "t_power_min",
                "regular_condition_PRISM_pctl": "t_power_min",
                "post_condition_unexp_pt": "(Load_Follow & (! Heatup))",
                "post_condition_unexp_ft": "(Load_Follow & (! Heatup))",
                "post_condition_unexp_pctl": "(Load_Follow & (! Heatup))",
                "post_condition_SMV_pt": "(Load_Follow & (! Heatup))",
                "post_condition_SMV_ft": "(Load_Follow & (! Heatup))",
                "post_condition_MLTL_ft": "(Load_Follow & (! Heatup))",
                "post_condition_PRISM_pctl": "(Load_Follow & (! Heatup))",
                "ft": "((LAST V ((! (Fin_Heatup & (! LAST))) | (X (((Lin_Heatup | LAST) V (((! t_power_min) & ((! LAST) & ((X t_power_min) & (! (Lin_Heatup | LAST))))) -> ((X ((Lin_Heatup | LAST) | (X (Load_Follow & (! Heatup))))) & (! (Lin_Heatup | LAST))))) & (t_power_min -> ((Lin_Heatup | LAST) | (X (Load_Follow & (! Heatup))))))))) & (Heatup -> (((Lin_Heatup | LAST) V (((! t_power_min) & ((! LAST) & ((X t_power_min) & (! (Lin_Heatup | LAST))))) -> ((X ((Lin_Heatup | LAST) | (X (Load_Follow & (! Heatup))))) & (! (Lin_Heatup | LAST))))) & (t_power_min -> ((Lin_Heatup | LAST) | (X (Load_Follow & (! Heatup))))))))",
                "pt": "((H (Lin_Heatup -> (Y (((Y (t_power_min & ((Y (! t_power_min)) | Fin_Heatup))) -> ((Load_Follow & (! Heatup)) | Fin_Heatup)) S (((Y (t_power_min & ((Y (! t_power_min)) | Fin_Heatup))) -> ((Load_Follow & (! Heatup)) | Fin_Heatup)) & Fin_Heatup))))) & (((! Lin_Heatup) S ((! Lin_Heatup) & Fin_Heatup)) -> (((Y (t_power_min & ((Y (! t_power_min)) | Fin_Heatup))) -> ((Load_Follow & (! Heatup)) | Fin_Heatup)) S (((Y (t_power_min & ((Y (! t_power_min)) | Fin_Heatup))) -> ((Load_Follow & (! Heatup)) | Fin_Heatup)) & Fin_Heatup))))",
                "pctl": "P>=1[((G ((! (Fin_Heatup & (! LAST))) | (X ((Lin_Heatup R (((! t_power_min) & ((X t_power_min) & (! Lin_Heatup))) => ((X (P>=1[(Lin_Heatup | ((X (Load_Follow & (! Heatup))) & (! Lin_Heatup)))])) & (! Lin_Heatup)))) & (t_power_min => (P>=1[(Lin_Heatup | ((X (Load_Follow & (! Heatup))) & (! Lin_Heatup)))])))))) & (Heatup => (Lin_Heatup | ((Lin_Heatup R (((! t_power_min) & ((X t_power_min) & (! Lin_Heatup))) => ((X (P>=1[(Lin_Heatup | ((X (Load_Follow & (! Heatup))) & (! Lin_Heatup)))])) & (! Lin_Heatup)))) & (t_power_min => (P>=1[(Lin_Heatup | ((X (Load_Follow & (! Heatup))) & (! Lin_Heatup)))]))))))]",
                "ptExpanded": "((H (((! Heatup) & (Y Heatup)) -> (Y (((Y (t_power_min & ((Y (! t_power_min)) | (Heatup & (Z (! Heatup)))))) -> ((Load_Follow & (! Heatup)) | (Heatup & (Z (! Heatup))))) S (((Y (t_power_min & ((Y (! t_power_min)) | (Heatup & (Z (! Heatup)))))) -> ((Load_Follow & (! Heatup)) | (Heatup & (Z (! Heatup))))) & (Heatup & (Z (! Heatup)))))))) & (((! ((! Heatup) & (Y Heatup))) S ((! ((! Heatup) & (Y Heatup))) & (Heatup & (Z (! Heatup))))) -> (((Y (t_power_min & ((Y (! t_power_min)) | (Heatup & (Z (! Heatup)))))) -> ((Load_Follow & (! Heatup)) | (Heatup & (Z (! Heatup))))) S (((Y (t_power_min & ((Y (! t_power_min)) | (Heatup & (Z (! Heatup)))))) -> ((Load_Follow & (! Heatup)) | (Heatup & (Z (! Heatup))))) & (Heatup & (Z (! Heatup)))))))",
                "CoCoSpecCode": "(H(((not (Heatup) and YtoPre(Heatup)) => YtoPre(SI((Heatup and ZtoPre(not (Heatup))),(YtoPre((t_power_min and (YtoPre(not (t_power_min)) or (Heatup and ZtoPre(not (Heatup)))))) => ((Load_Follow and not (Heatup)) or (Heatup and ZtoPre(not (Heatup))))))))) and (SI((Heatup and ZtoPre(not (Heatup))),not ((not (Heatup) and YtoPre(Heatup)))) => SI((Heatup and ZtoPre(not (Heatup))),(YtoPre((t_power_min and (YtoPre(not (t_power_min)) or (Heatup and ZtoPre(not (Heatup)))))) => ((Load_Follow and not (Heatup)) or (Heatup and ZtoPre(not (Heatup))))))))",
                "ftExpanded": "((LAST V ((! ((((! Heatup) & (! LAST)) & (X Heatup)) & (! LAST))) | (X (((((Heatup & (! LAST)) & (X (! Heatup))) | LAST) V (((! t_power_min) & ((! LAST) & ((X t_power_min) & (! (((Heatup & (! LAST)) & (X (! Heatup))) | LAST))))) -> ((X ((((Heatup & (! LAST)) & (X (! Heatup))) | LAST) | (X (Load_Follow & (! Heatup))))) & (! (((Heatup & (! LAST)) & (X (! Heatup))) | LAST))))) & (t_power_min -> ((((Heatup & (! LAST)) & (X (! Heatup))) | LAST) | (X (Load_Follow & (! Heatup))))))))) & (Heatup -> (((((Heatup & (! LAST)) & (X (! Heatup))) | LAST) V (((! t_power_min) & ((! LAST) & ((X t_power_min) & (! (((Heatup & (! LAST)) & (X (! Heatup))) | LAST))))) -> ((X ((((Heatup & (! LAST)) & (X (! Heatup))) | LAST) | (X (Load_Follow & (! Heatup))))) & (! (((Heatup & (! LAST)) & (X (! Heatup))) | LAST))))) & (t_power_min -> ((((Heatup & (! LAST)) & (X (! Heatup))) | LAST) | (X (Load_Follow & (! Heatup))))))))",
                "pctlExpanded": "P>=1[((G ((! (((! Heatup) & (X Heatup)) & (! false))) | (X (((Heatup & (X (! Heatup))) R (((! t_power_min) & ((X t_power_min) & (! (Heatup & (X (! Heatup)))))) => ((X (P>=1[((Heatup & (X (! Heatup))) | ((X (Load_Follow & (! Heatup))) & (! (Heatup & (X (! Heatup))))))])) & (! (Heatup & (X (! Heatup))))))) & (t_power_min => (P>=1[((Heatup & (X (! Heatup))) | ((X (Load_Follow & (! Heatup))) & (! (Heatup & (X (! Heatup))))))])))))) & (Heatup => ((Heatup & (X (! Heatup))) | (((Heatup & (X (! Heatup))) R (((! t_power_min) & ((X t_power_min) & (! (Heatup & (X (! Heatup)))))) => ((X (P>=1[((Heatup & (X (! Heatup))) | ((X (Load_Follow & (! Heatup))) & (! (Heatup & (X (! Heatup))))))])) & (! (Heatup & (X (! Heatup))))))) & (t_power_min => (P>=1[((Heatup & (X (! Heatup))) | ((X (Load_Follow & (! Heatup))) & (! (Heatup & (X (! Heatup))))))]))))))]",
                "ftInfAUExpanded": "((G ((! ((! Heatup) & (X Heatup))) | (X (((Heatup & (X (! Heatup))) V (((! t_power_min) & ((X t_power_min) & (! (Heatup & (X (! Heatup)))))) -> ((X ((Heatup & (X (! Heatup))) | (X (Load_Follow & (! Heatup))))) & (! (Heatup & (X (! Heatup))))))) & (t_power_min -> ((Heatup & (X (! Heatup))) | (X (Load_Follow & (! Heatup))))))))) & (Heatup -> (((Heatup & (X (! Heatup))) V (((! t_power_min) & ((X t_power_min) & (! (Heatup & (X (! Heatup)))))) -> ((X ((Heatup & (X (! Heatup))) | (X (Load_Follow & (! Heatup))))) & (! (Heatup & (X (! Heatup))))))) & (t_power_min -> ((Heatup & (X (! Heatup))) | (X (Load_Follow & (! Heatup))))))))",
                "mltlExpanded": "((G[0,M] (((p0 & ((! p1) & ((F[1,1] p1) & (F[1,1] p0)))) -> ((F[2,2] (! p0)) | (F[2,2] p2))) & (((! p0) & (F[1,1] p0)) -> (F[1,1] (p1 -> ((F[1,1] (! p0)) | (F[1,1] p2))))))) & ((p0 & p1) -> ((F[1,1] (! p0)) | (F[1,1] p2))))",
                "WESTMapping": "p0: Heatup<br/>p1: t_power_min<br/>p2: (Load_Follow & (! Heatup))",
                "R2U2Code": "((((Heatup && ((! t_power_min) && ((F[1,1] t_power_min) && (F[1,1] Heatup)))) -> ((F[2,2] (! Heatup)) || (F[2,2] (Load_Follow && (! Heatup))))) && (((! Heatup) && (F[1,1] Heatup)) -> (F[1,1] (t_power_min -> ((F[1,1] (! Heatup)) || (F[1,1] (Load_Follow && (! Heatup)))))))) && (((TAU == 0) && (Heatup && t_power_min)) -> ((F[1,1] (! Heatup)) || (F[1,1] (Load_Follow && (! Heatup))))))",
                "component": "DRC"
            },
            "_id": "c48fdfd0-2f92-11f1-bda7-b107d916a2e5"
        },
        {
            "reqid": "PWR-0000",
            "parent_reqid": "",
            "project": "PWR_Hybrid",
            "rationale": "",
            "comments": "",
            "fulltext": "DRC shall initially satisfy (Cold_Shutdown & !SCRAM)",
            "status": "",
            "semantics": {
                "type": "nasa",
                "scope": {
                    "type": "null"
                },
                "condition": "null",
                "probability": "null",
                "timing": "immediately",
                "response": "satisfaction",
                "variables": [
                    "Cold_Shutdown",
                    "SCRAM"
                ],
                "component_name": "DRC",
                "componentTextRange": [
                    0,
                    2
                ],
                "timingTextRange": [
                    10,
                    18
                ],
                "post_condition": "(( Cold_Shutdown & ! SCRAM ))",
                "responseTextRange": [
                    20,
                    51
                ],
                "diagramVariables": "Response = <b><i>(( Cold_Shutdown & ! 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, if trigger holds then <b><i>(( Cold_Shutdown & ! SCRAM ))</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>(( Cold_Shutdown & ! SCRAM ))</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": "(Cold_Shutdown & (! SCRAM))",
                "post_condition_unexp_ft": "(Cold_Shutdown & (! SCRAM))",
                "post_condition_unexp_pctl": "(Cold_Shutdown & (! SCRAM))",
                "post_condition_SMV_pt": "(Cold_Shutdown & (! SCRAM))",
                "post_condition_SMV_ft": "(Cold_Shutdown & (! SCRAM))",
                "post_condition_MLTL_ft": "(Cold_Shutdown & (! SCRAM))",
                "post_condition_PRISM_pctl": "(Cold_Shutdown & (! SCRAM))",
                "ft": "(Cold_Shutdown & (! SCRAM))",
                "pt": "(H ((Z FALSE) -> (Cold_Shutdown & (! SCRAM))))",
                "pctl": "(P>=1[(Cold_Shutdown & (! SCRAM))])",
                "ptExpanded": "(H ((Z FALSE) -> (Cold_Shutdown & (! SCRAM))))",
                "CoCoSpecCode": "H((ZtoPre(false) => (Cold_Shutdown and not (SCRAM))))",
                "ftExpanded": "(Cold_Shutdown & (! SCRAM))",
                "pctlExpanded": "(P>=1[(Cold_Shutdown & (! SCRAM))])",
                "ftInfAUExpanded": "(Cold_Shutdown & (! SCRAM))",
                "mltlExpanded": "p0",
                "WESTMapping": "p0: (Cold_Shutdown & (! SCRAM))",
                "R2U2Code": "((TAU == 0) -> (Cold_Shutdown && (! SCRAM)))",
                "component": "DRC"
            },
            "_id": "e4805020-2ec7-11f1-bda7-b107d916a2e5"
        },
        {
            "reqid": "PWR-0102",
            "parent_reqid": "",
            "project": "PWR_Hybrid",
            "rationale": "If scram is triggered, scram will always be triggered for the rest of time.",
            "comments": "",
            "fulltext": "If SCRAM DRC shall always satisfy SCRAM",
            "status": "",
            "semantics": {
                "type": "nasa",
                "scope": {
                    "type": "null"
                },
                "condition": "regular",
                "probability": "null",
                "timing": "always",
                "response": "satisfaction",
                "variables": [
                    "SCRAM"
                ],
                "qualifier_word": "if",
                "pre_condition": "(SCRAM)",
                "regular_condition": "(SCRAM)",
                "conditionTextRange": [
                    0,
                    7
                ],
                "component_name": "DRC",
                "componentTextRange": [
                    9,
                    11
                ],
                "timingTextRange": [
                    19,
                    24
                ],
                "post_condition": "(SCRAM)",
                "responseTextRange": [
                    26,
                    38
                ],
                "diagramVariables": "TC = <b><i>(SCRAM)</i></b>, Response = <b><i>(SCRAM)</i></b>.",
                "description": "SCOPE: in the interval defined by the entire execution.<br>TRIGGER: first point in the interval if <b><i>(SCRAM)</i></b> is true and any point in the interval where <b><i>(SCRAM)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, <b><i>(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 if <b><i>(SCRAM)</i></b> is true and any point in the interval where <b><i>(SCRAM)</i></b> becomes true (from false).<br>REQUIRED BEHAVIOR: for every trigger, with probability >=1, <b><i>(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_regular_always_satisfaction.svg",
                "scope_mode_pt": "BAD_PT",
                "scope_mode_ft": "BAD_FT",
                "regular_condition_unexp_pt": "SCRAM",
                "regular_condition_unexp_ft": "SCRAM",
                "regular_condition_unexp_pctl": "SCRAM",
                "regular_condition_SMV_pt": "SCRAM",
                "regular_condition_SMV_ft": "SCRAM",
                "regular_condition_MLTL_ft": "SCRAM",
                "regular_condition_PRISM_pctl": "SCRAM",
                "post_condition_unexp_pt": "SCRAM",
                "post_condition_unexp_ft": "SCRAM",
                "post_condition_unexp_pctl": "SCRAM",
                "post_condition_SMV_pt": "SCRAM",
                "post_condition_SMV_ft": "SCRAM",
                "post_condition_MLTL_ft": "SCRAM",
                "post_condition_PRISM_pctl": "SCRAM",
                "ft": "((LAST V (((! SCRAM) & ((! LAST) & (X SCRAM))) -> (X (LAST V SCRAM)))) & (SCRAM -> (LAST V SCRAM)))",
                "pt": "(H ((H (! SCRAM)) | SCRAM))",
                "pctl": "P>=1[((G (((! SCRAM) & (X SCRAM)) => (X (P>=1[(G SCRAM)])))) & (SCRAM => (P>=1[(G SCRAM)])))]",
                "ptExpanded": "(H ((H (! SCRAM)) | SCRAM))",
                "CoCoSpecCode": "H((H(not (SCRAM)) or SCRAM))",
                "ftExpanded": "((LAST V (((! SCRAM) & ((! LAST) & (X SCRAM))) -> (X (LAST V SCRAM)))) & (SCRAM -> (LAST V SCRAM)))",
                "pctlExpanded": "P>=1[((G (((! SCRAM) & (X SCRAM)) => (X (P>=1[(G SCRAM)])))) & (SCRAM => (P>=1[(G SCRAM)])))]",
                "ftInfAUExpanded": "((G (((! SCRAM) & (X SCRAM)) -> (X (G SCRAM)))) & (SCRAM -> (G SCRAM)))",
                "mltlExpanded": "((G[0,M] (((! p0) & (F[1,1] p0)) -> (G[1,M] p0))) & (p0 -> (G[0,M] p0)))",
                "WESTMapping": "p0: SCRAM",
                "R2U2Code": "((((! SCRAM) && (F[1,1] SCRAM)) -> (G[1,M] SCRAM)) && (((TAU == 0) && SCRAM) -> (G[0,M] SCRAM)))",
                "component": "DRC"
            },
            "_id": "e9c0c9f0-31df-11f1-820b-8f6ab14cd565"
        }
    ],
    "variables": [
        {
            "project": "PWR_Hybrid",
            "component_name": "DRC",
            "variable_name": "Cold_Shutdown",
            "reqs": [
                "3a0697b0-2f91-11f1-bda7-b107d916a2e5",
                "bfa3ea30-2f91-11f1-bda7-b107d916a2e5",
                "e4805020-2ec7-11f1-bda7-b107d916a2e5"
            ],
            "dataType": "boolean",
            "idType": "Output",
            "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_HybridDRCCold_Shutdown"
        },
        {
            "project": "PWR_Hybrid",
            "component_name": "DRC",
            "variable_name": "Heatup",
            "reqs": [
                "3a0697b0-2f91-11f1-bda7-b107d916a2e5",
                "50de1300-2fa0-11f1-b1b5-5117d78e7f0f",
                "a6665110-2f92-11f1-bda7-b107d916a2e5",
                "bfa3ea30-2f91-11f1-bda7-b107d916a2e5",
                "c48fdfd0-2f92-11f1-bda7-b107d916a2e5",
                "29bfe300-31e1-11f1-820b-8f6ab14cd565"
            ],
            "dataType": "boolean",
            "idType": "Output",
            "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_HybridDRCHeatup"
        },
        {
            "project": "PWR_Hybrid",
            "component_name": "DRC",
            "variable_name": "Load_Follow",
            "reqs": [
                "3a0697b0-2f91-11f1-bda7-b107d916a2e5",
                "50de1300-2fa0-11f1-b1b5-5117d78e7f0f",
                "c48fdfd0-2f92-11f1-bda7-b107d916a2e5",
                "29bfe300-31e1-11f1-820b-8f6ab14cd565"
            ],
            "dataType": "boolean",
            "idType": "Output",
            "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_HybridDRCLoad_Follow"
        },
        {
            "project": "PWR_Hybrid",
            "component_name": "DRC",
            "variable_name": "OP_MODE",
            "reqs": [
                "1af49c60-2f9f-11f1-bda7-b107d916a2e5",
                "3a0697b0-2f91-11f1-bda7-b107d916a2e5",
                "50de1300-2fa0-11f1-b1b5-5117d78e7f0f",
                "bfa3ea30-2f91-11f1-bda7-b107d916a2e5",
                "29bfe300-31e1-11f1-820b-8f6ab14cd565"
            ],
            "dataType": "boolean",
            "idType": "Output",
            "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_HybridDRCOP_MODE"
        },
        {
            "project": "PWR_Hybrid",
            "component_name": "DRC",
            "variable_name": "SCRAM",
            "reqs": [
                "1af49c60-2f9f-11f1-bda7-b107d916a2e5",
                "3a0697b0-2f91-11f1-bda7-b107d916a2e5",
                "96d7c900-2f96-11f1-bda7-b107d916a2e5",
                "a6665110-2f92-11f1-bda7-b107d916a2e5",
                "bfa3ea30-2f91-11f1-bda7-b107d916a2e5",
                "e4805020-2ec7-11f1-bda7-b107d916a2e5",
                "e9c0c9f0-31df-11f1-820b-8f6ab14cd565"
            ],
            "dataType": "boolean",
            "idType": "Output",
            "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_HybridDRCSCRAM"
        },
        {
            "project": "PWR_Hybrid",
            "component_name": "DRC",
            "variable_name": "STARTUP",
            "reqs": [
                "bfa3ea30-2f91-11f1-bda7-b107d916a2e5"
            ],
            "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_HybridDRCSTARTUP"
        },
        {
            "project": "PWR_Hybrid",
            "component_name": "DRC",
            "variable_name": "t_dot_exceeded",
            "reqs": [
                "a6665110-2f92-11f1-bda7-b107d916a2e5"
            ],
            "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_HybridDRCt_dot_exceeded"
        },
        {
            "project": "PWR_Hybrid",
            "component_name": "DRC",
            "variable_name": "t_max_exceeded",
            "reqs": [
                "96d7c900-2f96-11f1-bda7-b107d916a2e5"
            ],
            "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_HybridDRCt_max_exceeded"
        },
        {
            "project": "PWR_Hybrid",
            "component_name": "DRC",
            "variable_name": "t_power_min",
            "reqs": [
                "c48fdfd0-2f92-11f1-bda7-b107d916a2e5"
            ],
            "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_HybridDRCt_power_min"
        }
    ]
}