trace.tsx 8.22 KB
Newer Older
1
2
3
4
/* If we don't assign react useState variables within a render cycle, things break */
/* eslint-disable react-hooks/exhaustive-deps */

import React, { useCallback, useEffect, useState } from "react";
5
import { Button, Checkbox, Modal, ProgressBar } from "react-bootstrap";
Dominic's avatar
Dominic committed
6
import { LTSTransition } from "../../../../../../../../pseuco-shared-components/lts/lts";
7
8
import { TranslatorTraceReturndata } from "../../../../../../worker/translatorTrace";
import { StateKey } from "../../../../../editors/ltsEditor/ltsEditorTypes";
9
import { TranslatorWorkerConfiguration } from "../../../../../util/taskmanagerTypes";
10
import { pluralize } from "../../../../../utils";
Dominic's avatar
Dominic committed
11
import { ActionComponentAPI } from "../../ActionComponentHost";
12
import { ActionBehavior, DataActionComponent } from "../../actions";
13
import { renderTrace, TraceComputationState } from "./traceUtils";
14

Dominic's avatar
Dominic committed
15
16
import '../actions.css';

Dominic's avatar
Dominic committed
17
const DEFAULT_STEPCOUNT = 500;
18

19
export const TraceModal: DataActionComponent<{prefilledTrace?: LTSTransition[]}> = (props) => {
Dominic's avatar
Dominic committed
20
    const [show, setShow] = useState(true);
Dominic's avatar
Dominic committed
21
22
23
24
    const hideCallback = () => { cancel(); setShow(false); };

    const data = props.initializedDataAuthorityData.data.lts;
    const worker = props.initializedDataAuthorityData.api.worker;
25
    const prefilledTrace = props.prefilledTrace;
26
    const [focusedAction, setFocusedAction] = useState<LTSTransition["label"] | undefined>(prefilledTrace && prefilledTrace[prefilledTrace.length - 1].label);
27
28

    const [hideStates, setHideStates] = useState<boolean>(true);
29
    const [hideWeaks, setHideWeaks] = useState<boolean>(true);
Dominic's avatar
Dominic committed
30
31

    const initialState: StateKey | undefined = props.initializedDataAuthorityData.data.lts.core?.initialState;
32
    const [status, setStatus] = useState<TraceComputationState>("running");
33

Dominic's avatar
Dominic committed
34
    let [currentState, setCurrentState] = useState<string | undefined>(initialState);
35
    let [transitions, setTransitions] = useState<LTSTransition[]>(() =>
36
        []
37
    );
Dominic's avatar
Dominic committed
38

39
    const [error, setError] = useState<string | null>(null);
40

Dominic's avatar
Dominic committed
41
42
    const [traceTask, setTraceTask] = useState<number>();

43
44
    const numberWeakSteps = transitions.filter((transition) => !!transition.weak).length;

45
    const restart = useCallback(() => {
Dominic's avatar
Dominic committed
46
47
48
49
50
51
52
53
54
55
        if (!data.core) return;
        if (initialState) {
            setTransitions(transitions = []);
            setCurrentState(currentState = data.core.initialState);
            setError(null);
            setStatus("running");
            resume();
        } else {
            setStatus("error");
            setError("Your LTS contains no state.");
56
        }
57
    },[]);
Dominic's avatar
Dominic committed
58

59
    const cancel = useCallback(() => {
Dominic's avatar
Dominic committed
60
61
62
63
        if (traceTask !== undefined) {
            worker.cancelTask(traceTask);
        }
        setStatus("paused");
64
    }, [traceTask, worker]);
Dominic's avatar
Dominic committed
65

66
    useEffect(() => {
67
68
69
70
71
72
        if (prefilledTrace !== undefined) {
            if (prefilledTrace.length === 0) throw new Error("Prefilled trace had 0 elements, that's odd.");
            setTransitions(transitions = prefilledTrace);
            setFocusedAction(prefilledTrace[prefilledTrace.length - 1].label);
            setCurrentState(prefilledTrace[prefilledTrace.length - 1].target);
            setStatus("paused");
73
74
75
        } else {
            restart();
        }
76
        return cancel;
77
    }, []);
Dominic's avatar
Dominic committed
78
79
80
81
82
83

    const resume = (stepCount?: number) => {
        cancel();
        if (!stepCount) stepCount = DEFAULT_STEPCOUNT;
        if (data.extended.dataId === undefined) throw new Error("No dataID available!");
        if (!currentState) throw new Error("Trace has no state to resume exploration from");
84

Dominic's avatar
Dominic committed
85
        setStatus("running");
86

87
        const taskData : TranslatorWorkerConfiguration["trace"]["workerData"]= {
Dominic's avatar
Dominic committed
88
89
90
            stepCount: stepCount,
            dataId: data.extended.dataId,
            startState: currentState
91
        };
92
        const traceTaskId = worker.submitTask<"trace">('trace', taskData, (resultData, completed) => {
Dominic's avatar
Dominic committed
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
            if (completed && resultData === null) {
                // computation exceeded step count
                setTraceTask(undefined);
                setStatus("paused");
            }

            if (!resultData) return; // null-return -> ignore

            switch (resultData.command) {
                case 'failure':
                    setError("The trace could not be completed. Reason: " + resultData.error);
                    setStatus("error");
                    break;

                case 'completed':
                    //setTraceTerminated(true);
                    setStatus("completed");
                    break;

                case 'step':
                    transitions.push(resultData.transition);
                    setTransitions(transitions);
                    setCurrentState(resultData.transition.target);
                    break;

                default:
                    throw new Error("Unknown worker command!");
                //$location.path('/error').search({ error: 'unknownWorkerCommand', details: null });
            }
122
        }, () => {
Dominic's avatar
Dominic committed
123
124
            setStatus("paused");
            setTraceTask(undefined);
125
126
        }, 8);
        setTraceTask(traceTaskId);
Dominic's avatar
Dominic committed
127
    };
128

Dominic's avatar
Dominic committed
129
130
131
    if (prefilledTrace !== undefined && focusedAction == undefined) 
        throw new Error("A prefilled trace is provided, but the focusedAction is undefined!");

Dominic's avatar
Dominic committed
132
    return <Modal bsSize="large" show={show} onHide={hideCallback} onExited={props.destroyCallback}>
133
134
135
136
        <Modal.Header closeButton>
            <h2>Random Path</h2>
        </Modal.Header>
        <Modal.Body className="trace">
137
138
139
            {prefilledTrace === undefined ?
                <p>The following shows a random path throughout the LTS, until a terminal state is reached.</p>
                :
Dominic's avatar
Dominic committed
140
                <p>The following shows a random path throughout the LTS, eventually taking action <code>{focusedAction}</code>.</p>
141
            }
142
143
144
145
146
147
148
149
150
151
            <div className="form-group">
                <div className="checkbox">
                    <Checkbox onChange={() => setHideStates(!hideStates)} checked={hideStates}> only show the trace</Checkbox>
                </div>
                {hideStates ?
                    <div className="checkbox" ng-show="hideStates">
                        <Checkbox onChange={() => setHideWeaks(!hideWeaks)} checked={hideWeaks}> hide internal steps</Checkbox>
                    </div>
                    : null}
            </div>
152
153
154
155
            {prefilledTrace === undefined ?
                <Button bsStyle="warning" disabled={status === "running"} className="margin-right-10" onClick={restart}>Restart</Button>
                : null
            }
156
            {status === "running" ?
Dominic's avatar
Dominic committed
157
                <Button bsStyle="primary" onClick={cancel} >Pause computation</Button>
158
159
160
                : null}
            <hr/>
            <div>
Dominic's avatar
Dominic committed
161
                {renderTrace(transitions, initialState, !hideWeaks, !hideStates)}
162
163
164
165
166
167
168
169
170
                {status === "completed" ?
                    <div className="trace-termination"></div>
                    : null}
                {status === "error" ?
                    <div className="trace-error">{error}</div>
                    : null}
                {status === "paused" ?
                    <div className="trace-paused"></div>
                    : null}
Dominic's avatar
Dominic committed
171
                {hideStates && hideWeaks ?
172
173
174
175
176
177
178
179
180
181
182
183
184
185
                    <div>
                        {pluralize(
                            numberWeakSteps,
                            {
                                zero: "No internal steps are hidden.",
                                one: "One internal step is hidden.",
                                multiple: `${numberWeakSteps} internal steps are hidden.`
                            })}
                    </div>
                    : null}
                {status === "running" ?
                    <ProgressBar active now={100} />
                    : null}
                {status === "paused" ?
Dominic's avatar
Dominic committed
186
                    <Button onClick={() => resume()} bsStyle="primary" >Continue</Button>
187
188
189
190
                    : null}
            </div>
        </Modal.Body>
        <Modal.Footer>
Dominic's avatar
Dominic committed
191
            <Button onClick={hideCallback} bsStyle="primary">Close</Button>
192
193
194
195
        </Modal.Footer>
    </Modal>;
};

Dominic's avatar
Dominic committed
196
export const traceBehavior: ActionBehavior = (api: ActionComponentAPI) => {
197
    api.spawnComponent(TraceModal, { initializedDataAuthorityData: api.initializedDataAuthorityData });
198
};