diff --git a/frontend/package.json b/frontend/package.json
index c64943f..5914cb1 100644
--- a/frontend/package.json
+++ b/frontend/package.json
@@ -31,6 +31,7 @@
"@fontsource/roboto": "^4.5.8",
"@mui/material": "^5.11.4",
"react": "^18.2.0",
- "react-dom": "^18.2.0"
+ "react-dom": "^18.2.0",
+ "react-router-dom": "^6.10.0"
}
}
diff --git a/frontend/src/components/adf-details.tsx b/frontend/src/components/adf-details.tsx
new file mode 100644
index 0000000..8868b1a
--- /dev/null
+++ b/frontend/src/components/adf-details.tsx
@@ -0,0 +1,78 @@
+import React from 'react';
+
+import { AlertColor } from '@mui/material';
+
+import { GraphProps } from './graph-g6';
+
+export type Parsing = 'Naive' | 'Hybrid';
+
+export type StrategySnakeCase = 'parse_only' | 'ground' | 'complete' | 'stable' | 'stable_counting_a' | 'stable_counting_b' | 'stable_nogood';
+
+export type StrategyCamelCase = 'ParseOnly' | 'Ground' | 'Complete' | 'Stable' | 'StableCountingA' | 'StableCountingB' | 'StableNogood';
+
+export interface AcAndGraph {
+ ac: string[],
+ graph: GraphProps,
+}
+
+export type AcsWithGraphsOpt = {
+ type: 'None',
+} | {
+ type: 'Error',
+ content: string
+} | {
+ type: 'Some',
+ content: AcAndGraph[]
+};
+
+export type Task = {
+ type: 'Parse',
+} | {
+ type: 'Solve',
+ content: StrategyCamelCase,
+};
+
+export interface AdfProblemInfo {
+ name: string,
+ code: string,
+ parsing_used: Parsing,
+ // NOTE: the keys are really only strategies
+ acs_per_strategy: { [key in StrategySnakeCase]: AcsWithGraphsOpt },
+ running_tasks: Task[],
+}
+
+export function acsWithGraphOptToColor(status: AcsWithGraphsOpt, running: boolean): AlertColor {
+ if (running) {
+ return 'warning';
+ }
+
+ switch (status.type) {
+ case 'None': return 'info';
+ case 'Error': return 'error';
+ case 'Some': return 'success';
+ default:
+ throw new Error('Unknown type union variant (cannot occur)');
+ }
+}
+
+export function acsWithGraphOptToText(status: AcsWithGraphsOpt, running: boolean): string {
+ if (running) {
+ return 'Running';
+ }
+
+ switch (status.type) {
+ case 'None': return 'Not attempted';
+ case 'Error': return 'Failed';
+ case 'Some': return 'Done';
+ default:
+ throw new Error('Unknown type union variant (cannot occur)');
+ }
+}
+
+function AdfDetails() {
+ return (
+ Details
+ );
+}
+
+export default AdfDetails;
diff --git a/frontend/src/components/adf-new-form.tsx b/frontend/src/components/adf-new-form.tsx
new file mode 100644
index 0000000..e254bd1
--- /dev/null
+++ b/frontend/src/components/adf-new-form.tsx
@@ -0,0 +1,168 @@
+import React, {
+ useState, useContext, useCallback, useRef,
+} from 'react';
+
+import {
+ Button,
+ Container,
+ FormControl,
+ FormControlLabel,
+ FormLabel,
+ Link,
+ Paper,
+ Radio,
+ RadioGroup,
+ Stack,
+ Typography,
+ TextField,
+ ToggleButtonGroup,
+ ToggleButton,
+} from '@mui/material';
+
+import LoadingContext from './loading-context';
+import SnackbarContext from './snackbar-context';
+
+import { Parsing } from './adf-details';
+
+const PLACEHOLDER = `s(a).
+s(b).
+s(c).
+s(d).
+ac(a,c(v)).
+ac(b,b).
+ac(c,and(a,b)).
+ac(d,neg(b)).`;
+
+function AdfNewForm({ fetchProblems }: { fetchProblems: () => void; }) {
+ const { setLoading } = useContext(LoadingContext);
+ const { setStatus: setSnackbarInfo } = useContext(SnackbarContext);
+ const [isFileUpload, setFileUpload] = useState(false);
+ const [code, setCode] = useState(PLACEHOLDER);
+ const [filename, setFilename] = useState('');
+ const [parsing, setParsing] = useState('Naive');
+ const [name, setName] = useState('');
+ const fileRef = useRef(null);
+
+ const addAdf = useCallback(
+ () => {
+ setLoading(true);
+
+ const formData = new FormData();
+
+ if (isFileUpload && fileRef.current) {
+ const file = fileRef.current.files?.[0];
+ if (file) {
+ formData.append('file', file);
+ }
+ } else {
+ formData.append('code', code);
+ }
+
+ formData.append('parsing', parsing);
+ formData.append('name', name);
+
+ fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/adf/add`, {
+ method: 'POST',
+ credentials: process.env.NODE_ENV === 'development' ? 'include' : 'same-origin',
+ body: formData,
+ })
+ .then((res) => {
+ switch (res.status) {
+ case 200:
+ setSnackbarInfo({ message: 'Successfully added ADF problem!', severity: 'success', potentialUserChange: true });
+ fetchProblems();
+ break;
+ default:
+ setSnackbarInfo({ message: 'An error occured while adding the ADF problem.', severity: 'error', potentialUserChange: true });
+ break;
+ }
+ })
+ .finally(() => setLoading(false));
+ },
+ [isFileUpload, code, filename, parsing, name, fileRef.current],
+ );
+
+ return (
+
+
+
+ Add a new Problem
+
+
+
+ { setFileUpload(newValue); setFilename(''); }}
+ >
+
+ Write by Hand
+
+
+ Upload File
+
+
+
+
+
+
+ {isFileUpload ? (
+
+
+
+ ) : (
+
+ For more info on the syntax, have a
+ look
+ {' '}
+ here
+ .
+
+ )}
+ multiline
+ fullWidth
+ variant="filled"
+ value={code}
+ onChange={(event) => { setCode(event.target.value); }}
+ />
+ )}
+
+
+
+
+
+ Parsing Strategy
+ setParsing(((e.target as HTMLInputElement).value) as Parsing)}
+ >
+ } label="Naive" />
+ } label="Hybrid" />
+
+
+ { setName(event.target.value); }}
+ />
+
+
+
+
+
+ );
+}
+
+export default AdfNewForm;
diff --git a/frontend/src/components/adf-overview.tsx b/frontend/src/components/adf-overview.tsx
new file mode 100644
index 0000000..8b13dbf
--- /dev/null
+++ b/frontend/src/components/adf-overview.tsx
@@ -0,0 +1,164 @@
+import React, {
+ useRef, useState, useCallback, useEffect, useContext,
+} from 'react';
+
+import {
+ Chip,
+ Container,
+ Paper,
+ TableContainer,
+ Table,
+ TableHead,
+ TableRow,
+ TableCell,
+ TableBody,
+ Typography,
+} from '@mui/material';
+
+import AdfNewForm from './adf-new-form';
+
+import {
+ AdfProblemInfo,
+ StrategySnakeCase,
+ StrategyCamelCase,
+ Task,
+ acsWithGraphOptToColor,
+ acsWithGraphOptToText,
+} from './adf-details';
+
+import SnackbarContext from './snackbar-context';
+
+function AdfOverview() {
+ const { status: snackbarInfo } = useContext(SnackbarContext);
+ const [problems, setProblems] = useState([]);
+
+ const isFirstRender = useRef(true);
+
+ const fetchProblems = useCallback(
+ () => {
+ fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/adf/`, {
+ method: 'GET',
+ credentials: process.env.NODE_ENV === 'development' ? 'include' : 'same-origin',
+ headers: {
+ 'Content-Type': 'application/json',
+ },
+ })
+ .then((res) => {
+ switch (res.status) {
+ case 200:
+ res.json().then((resProblems) => {
+ setProblems(resProblems);
+ });
+ break;
+ case 401:
+ setProblems([]);
+ break;
+ default:
+ break;
+ }
+ });
+ },
+ [setProblems],
+ );
+
+ useEffect(
+ () => {
+ // TODO: having the info if the user may have changed on the snackbar info
+ // is a bit lazy and unclean; be better!
+ if (isFirstRender.current || snackbarInfo?.potentialUserChange) {
+ isFirstRender.current = false;
+
+ fetchProblems();
+ }
+ },
+ [snackbarInfo?.potentialUserChange],
+ );
+
+ useEffect(
+ () => {
+ // if there is a running task, fetch problems again after 20 seconds
+ let timeout: ReturnType;
+ if (problems.some((p) => p.running_tasks.length > 0)) {
+ timeout = setTimeout(() => fetchProblems(), 20000);
+ }
+
+ return () => {
+ if (timeout) {
+ clearTimeout(timeout);
+ }
+ };
+ },
+ [problems],
+ );
+
+ return (
+ <>
+
+ ADF-BDD.DEV
+
+ {problems.length > 0
+ && (
+
+
+
+ Existing Problems
+
+
+
+
+
+ ADF Problem Name
+ Parse Status
+ Grounded Solution
+ Complete Solution
+ Stable Solution
+ Stable Solution (Counting Method A)
+ Stable Solution (Counting Method B)
+ Stable Solution (Nogood-Based)
+
+
+
+ {problems.map((problem) => (
+
+
+ {problem.name}
+
+ {
+ (() => {
+ const status = problem.acs_per_strategy.parse_only;
+ const running = problem.running_tasks.some((t: Task) => t.type === 'Parse');
+
+ const color = acsWithGraphOptToColor(status, running);
+ const text = acsWithGraphOptToText(status, running);
+
+ return ;
+ })()
+ }
+ {
+ (['Ground', 'Complete', 'Stable', 'StableCountingA', 'StableCountingB', 'StableNogood'] as StrategyCamelCase[]).map((strategy) => {
+ const status = problem.acs_per_strategy[strategy.replace(/^([A-Z])/, (_, p1) => p1.toLowerCase()).replace(/([A-Z])/g, (_, p1) => `_${p1.toLowerCase()}`) as StrategySnakeCase];
+ const running = problem.running_tasks.some((t: Task) => t.type === 'Solve' && t.content === strategy);
+
+ const color = acsWithGraphOptToColor(status, running);
+ const text = acsWithGraphOptToText(status, running);
+
+ return ;
+ })
+ }
+
+ ))}
+
+
+
+
+
+ )}
+
+
+ );
+}
+
+export default AdfOverview;
diff --git a/frontend/src/components/app.tsx b/frontend/src/components/app.tsx
index b312717..bd6b9f8 100644
--- a/frontend/src/components/app.tsx
+++ b/frontend/src/components/app.tsx
@@ -1,180 +1,83 @@
-import * as React from 'react';
+import React, { useState, useMemo } from 'react';
+
+import { createBrowserRouter, RouterProvider } from 'react-router-dom';
import { ThemeProvider, createTheme } from '@mui/material/styles';
import {
+ Alert,
+ AlertColor,
Backdrop,
- Button,
CircularProgress,
CssBaseline,
- Container,
- FormControl,
- FormControlLabel,
- FormLabel,
- Link,
- Pagination,
- Paper,
- Radio,
- RadioGroup,
- Typography,
- TextField,
+ Snackbar,
+ useMediaQuery,
} from '@mui/material';
import LoadingContext from './loading-context';
-import GraphG6, { GraphProps } from './graph-g6';
+import SnackbarContext from './snackbar-context';
import Footer from './footer';
+import AdfOverview from './adf-overview';
+import AdfDetails from './adf-details';
-const { useState, useCallback, useMemo } = React;
-
-const darkTheme = createTheme({
- palette: {
- mode: 'dark',
+const browserRouter = createBrowserRouter([
+ {
+ path: '/',
+ element: ,
},
-});
-
-const placeholder = `s(a).
-s(b).
-s(c).
-s(d).
-ac(a,c(v)).
-ac(b,b).
-ac(c,and(a,b)).
-ac(d,neg(b)).`;
-
-enum Parsing {
- Naive = 'Naive',
- Hybrid = 'Hybrid',
-}
-
-enum Strategy {
- ParseOnly = 'ParseOnly',
- Ground = 'Ground',
- Complete = 'Complete',
- Stable = 'Stable',
- StableCountingA = 'StableCountingA',
- StableCountingB = 'StableCountingB',
- StableNogood = 'StableNogood',
-}
+ {
+ path: '/:adfName',
+ element: ,
+ },
+]);
function App() {
- const [loading, setLoading] = useState(false);
- const [code, setCode] = useState(placeholder);
- const [parsing, setParsing] = useState(Parsing.Naive);
- const [graphs, setGraphs] = useState();
- const [graphIndex, setGraphIndex] = useState(0);
+ const prefersDarkMode = useMediaQuery('(prefers-color-scheme: dark)');
- const submitHandler = useCallback(
- (strategy: Strategy) => {
- setLoading(true);
-
- fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/solve`, {
- method: 'POST',
- headers: {
- 'Content-Type': 'application/json',
- },
- body: JSON.stringify({ code, strategy, parsing }),
- })
- .then((res) => res.json())
- .then((data) => {
- setGraphs(data);
- setGraphIndex(0);
- })
- .finally(() => setLoading(false));
- // TODO: error handling
- },
- [code, parsing],
+ const theme = useMemo(
+ () => createTheme({
+ palette: {
+ mode: prefersDarkMode ? 'dark' : 'light',
+ },
+ }),
+ [prefersDarkMode],
);
+ const [loading, setLoading] = useState(false);
const loadingContext = useMemo(() => ({ loading, setLoading }), [loading, setLoading]);
+ const [snackbarInfo, setSnackbarInfo] = useState<{
+ message: string,
+ severity: AlertColor,
+ potentialUserChange: boolean,
+ } | undefined>();
+ const snackbarContext = useMemo(
+ () => ({ status: snackbarInfo, setStatus: setSnackbarInfo }),
+ [snackbarInfo, setSnackbarInfo],
+ );
+
return (
-
+
-
-
-
- Solve your ADF Problem with OBDDs!
-
+
+
+
+
+
+
-
-
- For more info on the syntax, have a
- look
- {' '}
- here
- .
-
- )}
- multiline
- fullWidth
- variant="filled"
- value={code}
- onChange={(event) => { setCode(event.target.value); }}
- />
-
-
-
- Parsing Strategy
- setParsing(((e.target as HTMLInputElement).value) as Parsing)}
- >
- } label="Naive" />
- } label="Hybrid" />
-
-
-
-
-
- {' '}
-
- {' '}
-
- {' '}
-
- {' '}
-
- {' '}
-
- {' '}
-
-
-
- {graphs
- && (
-
- {graphs.length > 1
- && (
- <>
- Models:
-
- setGraphIndex(value - 1)} />
-
- )}
- {graphs.length > 0
- && (
-
-
-
- )}
- {graphs.length === 0
- && <>No models!}
-
- )}
-
-
-
-
-
-
+
+
+
+ setSnackbarInfo(undefined)}
+ >
+ {snackbarInfo?.message}
+
+
);
diff --git a/frontend/src/components/footer.tsx b/frontend/src/components/footer.tsx
index 6055d1d..80d9645 100644
--- a/frontend/src/components/footer.tsx
+++ b/frontend/src/components/footer.tsx
@@ -1,5 +1,5 @@
import React, {
- useState, useCallback, useContext, useEffect,
+ useState, useCallback, useContext, useEffect, useRef,
} from 'react';
import {
@@ -11,12 +11,12 @@ import {
DialogActions,
DialogContent,
DialogTitle,
- Snackbar,
TextField,
Toolbar,
} from '@mui/material';
import LoadingContext from './loading-context';
+import SnackbarContext from './snackbar-context';
enum UserFormType {
Login = 'Login',
@@ -77,7 +77,7 @@ function UserForm({ username: propUsername, formType, close }: UserFormProps) {
.then((res) => {
switch (res.status) {
case 200:
- close(`Action '${formType}' successful!`, 'success');
+ close(`Action '${del ? 'Delete' : formType}' successful!`, 'success');
break;
default:
setError(true);
@@ -113,13 +113,14 @@ function UserForm({ username: propUsername, formType, close }: UserFormProps) {
-
+
{formType === UserFormType.Update
// TODO: add another confirm dialog here
&& (