Update Dockerfile

.dockerignore

@@ -1,4 +1,5 @@
 frontend/node_modules
 frontend/.parcel-cache
+server/mongodb-data
 target/debug
 

Cargo.lock

@@ -122,6 +122,44 @@ dependencies = [
  "syn 1.0.109",
 ]
 
+[[package]]
+name = "actix-multipart"
+version = "0.6.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dee489e3c01eae4d1c35b03c4493f71cb40d93f66b14558feb1b1a807671cc4e"
+dependencies = [
+ "actix-multipart-derive",
+ "actix-utils",
+ "actix-web",
+ "bytes",
+ "derive_more",
+ "futures-core",
+ "futures-util",
+ "httparse",
+ "local-waker",
+ "log",
+ "memchr",
+ "mime",
+ "serde",
+ "serde_json",
+ "serde_plain",
+ "tempfile",
+ "tokio",
+]
+
+[[package]]
+name = "actix-multipart-derive"
+version = "0.6.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2ec592f234db8a253cf80531246a4407c8a70530423eea80688a6c5a44a110e7"
+dependencies = [
+ "darling 0.14.4",
+ "parse-size",
+ "proc-macro2",
+ "quote",
+ "syn 1.0.109",
+]
+
 [[package]]
 name = "actix-router"
 version = "0.5.1"
@@ -278,6 +316,7 @@ dependencies = [
  "actix-cors",
  "actix-files",
  "actix-identity",
+ "actix-multipart",
  "actix-session",
  "actix-web",
  "adf_bdd",
@@ -918,8 +957,18 @@ version = "0.13.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "a01d95850c592940db9b8194bc39f4bc0e89dee5c4265e4b1807c34a9aba453c"
 dependencies = [
- "darling_core",
+ "darling_core 0.13.4",
- "darling_macro",
+ "darling_macro 0.13.4",
+]
+
+[[package]]
+name = "darling"
+version = "0.14.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7b750cb3417fd1b327431a470f388520309479ab0bf5e323505daf0290cd3850"
+dependencies = [
+ "darling_core 0.14.4",
+ "darling_macro 0.14.4",
 ]
 
 [[package]]
@@ -936,13 +985,38 @@ dependencies = [
  "syn 1.0.109",
 ]
 
+[[package]]
+name = "darling_core"
+version = "0.14.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "109c1ca6e6b7f82cc233a97004ea8ed7ca123a9af07a8230878fcfda9b158bf0"
+dependencies = [
+ "fnv",
+ "ident_case",
+ "proc-macro2",
+ "quote",
+ "strsim",
+ "syn 1.0.109",
+]
+
 [[package]]
 name = "darling_macro"
 version = "0.13.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "9c972679f83bdf9c42bd905396b6c3588a843a17f0f16dfcfa3e2c5d57441835"
 dependencies = [
- "darling_core",
+ "darling_core 0.13.4",
+ "quote",
+ "syn 1.0.109",
+]
+
+[[package]]
+name = "darling_macro"
+version = "0.14.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a4aab4dbc9f7611d8b55048a3a16d2d010c2c8334e46304b40ac1cc14bf3b48e"
+dependencies = [
+ "darling_core 0.14.4",
  "quote",
  "syn 1.0.109",
 ]
@@ -1881,6 +1955,12 @@ dependencies = [
  "windows-sys 0.45.0",
 ]
 
+[[package]]
+name = "parse-size"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "944553dd59c802559559161f9816429058b869003836120e262e8caec061b7ae"
+
 [[package]]
 name = "password-hash"
 version = "0.5.0"
@@ -2339,6 +2419,15 @@ dependencies = [
  "serde",
 ]
 
+[[package]]
+name = "serde_plain"
+version = "1.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d6018081315db179d0ce57b1fe4b62a12a0028c9cf9bbef868c9cf477b3c34ae"
+dependencies = [
+ "serde",
+]
+
 [[package]]
 name = "serde_urlencoded"
 version = "0.7.1"
@@ -2367,7 +2456,7 @@ version = "1.5.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "e182d6ec6f05393cc0e5ed1bf81ad6db3a8feedf8ee515ecdd369809bcce8082"
 dependencies = [
- "darling",
+ "darling 0.13.4",
  "proc-macro2",
  "quote",
  "syn 1.0.109",

Dockerfile

@@ -1,5 +1,5 @@
 # 1. BUILD-CONTAINER: Frontend
-FROM node:gallium-alpine
+FROM node:hydrogen-alpine
 
 WORKDIR /root
 
@@ -30,5 +30,7 @@ WORKDIR /root
 COPY --from=0 /root/dist /root/assets
 COPY --from=1 /root/target/release/adf-bdd-server /root/server
 
+EXPOSE 8080
+
 ENTRYPOINT ["./server"]
 

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"
     }
 }

frontend/src/components/adf-details.tsx

@@ -0,0 +1,341 @@
+import React, {
+  useState, useContext, useEffect, useCallback, useRef,
+} from 'react';
+import { useParams, useNavigate } from 'react-router-dom';
+import {
+  Alert,
+  AlertColor,
+  Button,
+  Chip,
+  Container,
+  Paper,
+  Pagination,
+  Skeleton,
+  Stack,
+  Tabs,
+  Tab,
+  TextField,
+  Typography,
+} from '@mui/material';
+
+import GraphG6, { GraphProps } from './graph-g6';
+import LoadingContext from './loading-context';
+import SnackbarContext from './snackbar-context';
+
+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 const STRATEGIES_WITHOUT_PARSE: StrategyCamelCase[] = ['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() {
+  const { adfName } = useParams();
+  const navigate = useNavigate();
+
+  const { setLoading } = useContext(LoadingContext);
+  const { status: snackbarInfo, setStatus: setSnackbarInfo } = useContext(SnackbarContext);
+  const [problem, setProblem] = useState<AdfProblemInfo>();
+  const [tab, setTab] = useState<StrategySnakeCase>('parse_only');
+  const [solutionIndex, setSolutionIndex] = useState<number>(0);
+
+  const isFirstRender = useRef(true);
+
+  const fetchProblem = useCallback(
+    () => {
+      fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/adf/${adfName}`, {
+        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((resProblem) => {
+                setProblem(resProblem);
+              });
+              break;
+            default:
+              navigate('/');
+              break;
+          }
+        });
+    },
+    [setProblem],
+  );
+
+  const solveHandler = useCallback(
+    (strategy: StrategyCamelCase) => {
+      setLoading(true);
+
+      fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/adf/${adfName}/solve`, {
+        method: 'PUT',
+        credentials: process.env.NODE_ENV === 'development' ? 'include' : 'same-origin',
+        headers: {
+          'Content-Type': 'application/json',
+        },
+        body: JSON.stringify({ strategy }),
+      })
+        .then((res) => {
+          switch (res.status) {
+            case 200:
+              setSnackbarInfo({ message: 'Solving problem now...', severity: 'success', potentialUserChange: false });
+              fetchProblem();
+              break;
+            default:
+              setSnackbarInfo({ message: 'Something went wrong tying to solve the problem.', severity: 'error', potentialUserChange: false });
+              break;
+          }
+        })
+        .finally(() => setLoading(false));
+    },
+    [adfName],
+  );
+
+  const deleteHandler = useCallback(
+    () => {
+      setLoading(true);
+
+      fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/adf/${adfName}`, {
+        method: 'DELETE',
+        credentials: process.env.NODE_ENV === 'development' ? 'include' : 'same-origin',
+        headers: {
+          'Content-Type': 'application/json',
+        },
+      })
+        .then((res) => {
+          switch (res.status) {
+            case 200:
+              setSnackbarInfo({ message: 'ADF Problem deleted.', severity: 'success', potentialUserChange: false });
+              navigate('/');
+              break;
+            default:
+              break;
+          }
+        })
+        .finally(() => setLoading(false));
+    },
+    [adfName],
+  );
+
+  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;
+
+        fetchProblem();
+      }
+    },
+    [snackbarInfo?.potentialUserChange],
+  );
+
+  useEffect(
+    () => {
+      // if there is a running task, fetch problems again after 20 seconds
+      let timeout: ReturnType<typeof setTimeout>;
+      if (problem && problem.running_tasks.length > 0) {
+        timeout = setTimeout(() => fetchProblem(), 20000);
+      }
+
+      return () => {
+        if (timeout) {
+          clearTimeout(timeout);
+        }
+      };
+    },
+    [problem],
+  );
+
+  const acsOpt = problem?.acs_per_strategy[tab];
+  const acsContent = acsOpt?.type === 'Some' ? acsOpt.content : undefined;
+  const tabCamelCase: StrategyCamelCase = tab.replace(/^([a-z])/, (_, p1) => p1.toUpperCase()).replace(/_([a-z])/g, (_, p1) => `${p1.toUpperCase()}`) as StrategyCamelCase;
+
+  return (
+    <>
+      <Typography variant="h3" component="h1" align="center" gutterBottom>
+        ADF-BDD.DEV
+      </Typography>
+      <Container sx={{ marginBottom: 4 }}>
+        {problem ? (
+          <>
+            <Paper elevation={8} sx={{ padding: 2, marginBottom: 2 }}>
+              <Stack direction="row" justifyContent="space-between" sx={{ marginBottom: 1 }}>
+                <Button
+                  variant="outlined"
+                  color="info"
+                  onClick={() => { navigate('/'); }}
+                >
+                  Back
+                </Button>
+                <Typography variant="h4" component="h2" align="center" gutterBottom>
+                  {problem.name}
+                </Typography>
+                <Button
+                  type="button"
+                  variant="outlined"
+                  color="error"
+                  onClick={() => {
+                  // eslint-disable-next-line no-alert
+                    if (window.confirm('Are you sure that you want to delete this ADF problem?')) {
+                      deleteHandler();
+                    }
+                  }}
+                >
+                  Delete
+                </Button>
+              </Stack>
+              <TextField
+                name="code"
+                label="Code"
+                helperText="Click here to copy!"
+                multiline
+                maxRows={5}
+                fullWidth
+                variant="filled"
+                value={problem.code.trim()}
+                disabled
+                sx={{ cursor: 'pointer' }}
+                onClick={() => { navigator.clipboard.writeText(problem.code); setSnackbarInfo({ message: 'Code copied to clipboard!', severity: 'info', potentialUserChange: false }); }}
+              />
+            </Paper>
+            <Tabs
+              value={tab}
+              onChange={(_e, newTab) => { setTab(newTab); setSolutionIndex(0); }}
+              variant="scrollable"
+              scrollButtons="auto"
+            >
+              <Tab wrapped value="parse_only" label={<Chip color={acsWithGraphOptToColor(problem.acs_per_strategy.parse_only, problem.running_tasks.some((t: Task) => t.type === 'Parse'))} label={`${problem.parsing_used} Parsing`} sx={{ cursor: 'inherit' }} />} />
+              {STRATEGIES_WITHOUT_PARSE.map((strategy) => {
+                const spaced = strategy.replace(/([A-Za-z])([A-Z])/g, '$1 $2');
+                const snakeCase = strategy.replace(/^([A-Z])/, (_, p1) => p1.toLowerCase()).replace(/([A-Z])/g, (_, p1) => `_${p1.toLowerCase()}`) as StrategySnakeCase;
+                const status = problem.acs_per_strategy[snakeCase];
+
+                const running = problem.running_tasks.some((t: Task) => t.type === 'Solve' && t.content === strategy);
+
+                const color = acsWithGraphOptToColor(status, running);
+
+                return <Tab key={strategy} wrapped value={snakeCase} label={<Chip color={color} label={spaced} sx={{ cursor: 'inherit' }} />} />;
+              })}
+            </Tabs>
+
+            {acsContent && acsContent.length > 1 && (
+              <>
+                Models:
+                <br />
+                <Pagination variant="outlined" shape="rounded" count={acsContent.length} page={solutionIndex + 1} onChange={(_e, newIdx) => setSolutionIndex(newIdx - 1)} />
+              </>
+            )}
+            <Paper elevation={3} square sx={{ padding: 2, marginTop: 4, marginBottom: 4 }}>
+              {problem.running_tasks.some((t: Task) => (tab === 'parse_only' && t.type === 'Parse') || (t.type === 'Solve' && t.content === tabCamelCase)) ? (
+                <Alert severity="warning">Working hard to solve the problem right now...</Alert>
+              ) : (
+                <>
+                  {acsContent && acsContent.length > 0 && (
+                  <GraphG6 graph={acsContent[solutionIndex].graph} />
+                  )}
+                  {acsContent && acsContent.length === 0 && (
+                  <Alert severity="info">The problem has no models for this strategy.</Alert>
+                  )}
+                  {!acsContent && acsOpt?.type === 'Error' && (
+                  <Alert severity="error">
+                    An error occurred:
+                    {acsOpt.content}
+                  </Alert>
+                  )}
+                  {!acsContent && acsOpt?.type === 'None' && (
+                  <>
+                    <Alert severity="info" sx={{ marginBottom: 1 }}>This strategy was not attempted yet.</Alert>
+                    <Button
+                      variant="contained"
+                      size="large"
+                      color="warning"
+                      onClick={() => {
+                        solveHandler(tabCamelCase);
+                      }}
+                    >
+                      Solve now!
+                    </Button>
+                  </>
+                  )}
+                </>
+              )}
+            </Paper>
+          </>
+        ) : (
+          <>
+            <Paper elevation={8} sx={{ padding: 2, marginBottom: 8 }}>
+              <Skeleton variant="text" width="50%" sx={{ fontSize: '2.125rem', margin: 'auto' }} />
+              <Skeleton variant="rounded" width="100%" height={200} />
+            </Paper>
+            <Skeleton variant="rectangular" width="100%" height={500} />
+          </>
+        )}
+      </Container>
+    </>
+  );
+}
+
+export default AdfDetails;

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<Parsing>('Naive');
+  const [name, setName] = useState('');
+  const fileRef = useRef<HTMLInputElement>(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 (
+    <Container>
+      <Paper elevation={8} sx={{ padding: 2 }}>
+        <Typography variant="h4" component="h2" align="center" gutterBottom>
+          Add a new Problem
+        </Typography>
+        <Container sx={{ marginTop: 2, marginBottom: 2 }}>
+          <Stack direction="row" justifyContent="center">
+            <ToggleButtonGroup
+              value={isFileUpload}
+              exclusive
+              onChange={(_e, newValue) => { setFileUpload(newValue); setFilename(''); }}
+            >
+              <ToggleButton value={false}>
+                Write by Hand
+              </ToggleButton>
+              <ToggleButton value>
+                Upload File
+              </ToggleButton>
+            </ToggleButtonGroup>
+          </Stack>
+        </Container>
+
+        <Container sx={{ marginTop: 2, marginBottom: 2 }}>
+          {isFileUpload ? (
+            <Stack direction="row" justifyContent="center">
+              <Button component="label">
+                {(!!filename && fileRef?.current?.files?.[0]) ? `File '${filename.split(/[\\/]/).pop()}' selected! (Click to change)` : 'Upload File'}
+                <input hidden type="file" onChange={(event) => { setFilename(event.target.value); }} ref={fileRef} />
+              </Button>
+            </Stack>
+          ) : (
+            <TextField
+              name="code"
+              label="Put your code here:"
+              helperText={(
+                <>
+                  For more info on the syntax, have a
+                  look
+                  {' '}
+                  <Link href="https://github.com/ellmau/adf-obdd" target="_blank" rel="noreferrer">here</Link>
+                  .
+                </>
+              )}
+              multiline
+              fullWidth
+              variant="filled"
+              value={code}
+              onChange={(event) => { setCode(event.target.value); }}
+            />
+          )}
+        </Container>
+
+        <Container sx={{ marginTop: 2 }}>
+          <Stack direction="row" justifyContent="center" spacing={2}>
+            <FormControl>
+              <FormLabel id="parsing-radio-group">Parsing Strategy</FormLabel>
+              <RadioGroup
+                row
+                aria-labelledby="parsing-radio-group"
+                name="parsing"
+                value={parsing}
+                onChange={(e) => setParsing(((e.target as HTMLInputElement).value) as Parsing)}
+              >
+                <FormControlLabel value="Naive" control={<Radio />} label="Naive" />
+                <FormControlLabel value="Hybrid" control={<Radio />} label="Hybrid" />
+              </RadioGroup>
+            </FormControl>
+            <TextField
+              name="name"
+              label="Adf Problem Name (optional):"
+              variant="standard"
+              value={name}
+              onChange={(event) => { setName(event.target.value); }}
+            />
+            <Button variant="outlined" onClick={() => addAdf()}>Add Adf Problem</Button>
+          </Stack>
+        </Container>
+      </Paper>
+    </Container>
+  );
+}
+
+export default AdfNewForm;

frontend/src/components/adf-overview.tsx

@@ -0,0 +1,171 @@
+import React, {
+  useRef, useState, useCallback, useEffect, useContext,
+} from 'react';
+
+import {
+  useNavigate,
+} from 'react-router-dom';
+
+import {
+  Chip,
+  Container,
+  Paper,
+  TableContainer,
+  Table,
+  TableHead,
+  TableRow,
+  TableCell,
+  TableBody,
+  Typography,
+} from '@mui/material';
+
+import AdfNewForm from './adf-new-form';
+
+import {
+  AdfProblemInfo,
+  StrategySnakeCase,
+  STRATEGIES_WITHOUT_PARSE,
+  Task,
+  acsWithGraphOptToColor,
+  acsWithGraphOptToText,
+} from './adf-details';
+
+import SnackbarContext from './snackbar-context';
+
+function AdfOverview() {
+  const { status: snackbarInfo } = useContext(SnackbarContext);
+  const [problems, setProblems] = useState<AdfProblemInfo[]>([]);
+
+  const navigate = useNavigate();
+
+  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<typeof setTimeout>;
+      if (problems.some((p) => p.running_tasks.length > 0)) {
+        timeout = setTimeout(() => fetchProblems(), 20000);
+      }
+
+      return () => {
+        if (timeout) {
+          clearTimeout(timeout);
+        }
+      };
+    },
+    [problems],
+  );
+
+  return (
+    <>
+      <Typography variant="h3" component="h1" align="center" gutterBottom>
+        ADF-BDD.DEV
+      </Typography>
+      {problems.length > 0
+        && (
+        <Container sx={{ marginBottom: 4 }}>
+          <Paper elevation={8} sx={{ padding: 2 }}>
+            <Typography variant="h4" component="h2" align="center" gutterBottom>
+              Existing Problems
+            </Typography>
+            <TableContainer component={Paper}>
+              <Table>
+                <TableHead>
+                  <TableRow>
+                    <TableCell align="center">ADF Problem Name</TableCell>
+                    <TableCell align="center">Parse Status</TableCell>
+                    <TableCell align="center">Grounded Solution</TableCell>
+                    <TableCell align="center">Complete Solution</TableCell>
+                    <TableCell align="center">Stable Solution</TableCell>
+                    <TableCell align="center">Stable Solution (Counting Method A)</TableCell>
+                    <TableCell align="center">Stable Solution (Counting Method B)</TableCell>
+                    <TableCell align="center">Stable Solution (Nogood-Based)</TableCell>
+                  </TableRow>
+                </TableHead>
+                <TableBody>
+                  {problems.map((problem) => (
+                    <TableRow
+                      key={problem.name}
+                      onClick={() => { navigate(`/${problem.name}`); }}
+                      sx={{ '&:last-child td, &:last-child th': { border: 0 }, cursor: 'pointer' }}
+                    >
+                      <TableCell component="th" scope="row">
+                        {problem.name}
+                      </TableCell>
+                      {
+                (() => {
+                  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 <TableCell align="center"><Chip color={color} label={`${text} (${problem.parsing_used} Parsing)`} sx={{ cursor: 'inherit' }} /></TableCell>;
+                })()
+              }
+                      {
+                  STRATEGIES_WITHOUT_PARSE.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 <TableCell key={strategy} align="center"><Chip color={color} label={text} sx={{ cursor: 'inherit' }} /></TableCell>;
+                  })
+              }
+                    </TableRow>
+                  ))}
+                </TableBody>
+              </Table>
+            </TableContainer>
+          </Paper>
+        </Container>
+        )}
+      <AdfNewForm fetchProblems={fetchProblems} />
+    </>
+  );
+}
+
+export default AdfOverview;

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,
+  Snackbar,
-  FormControl,
+  useMediaQuery,
-  FormControlLabel,
-  FormLabel,
-  Link,
-  Pagination,
-  Paper,
-  Radio,
-  RadioGroup,
-  Typography,
-  TextField,
 } 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 browserRouter = createBrowserRouter([
-
+  {
-const darkTheme = createTheme({
+    path: '/',
-  palette: {
+    element: <AdfOverview />,
-    mode: 'dark',
   },
-});
+  {
-
+    path: '/:adfName',
-const placeholder = `s(a).
+    element: <AdfDetails />,
-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',
-}
 
 function App() {
-  const [loading, setLoading] = useState(false);
+  const prefersDarkMode = useMediaQuery('(prefers-color-scheme: dark)');
-  const [code, setCode] = useState(placeholder);
-  const [parsing, setParsing] = useState(Parsing.Naive);
-  const [graphs, setGraphs] = useState<GraphProps[]>();
-  const [graphIndex, setGraphIndex] = useState(0);
 
-  const submitHandler = useCallback(
+  const theme = useMemo(
-    (strategy: Strategy) => {
+    () => createTheme({
-      setLoading(true);
+      palette: {
-
+        mode: prefersDarkMode ? 'dark' : 'light',
-      fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/solve`, {
+      },
-        method: 'POST',
+    }),
-        headers: {
+    [prefersDarkMode],
-          '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 [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 (
-    <ThemeProvider theme={darkTheme}>
+    <ThemeProvider theme={theme}>
       <LoadingContext.Provider value={loadingContext}>
-        <CssBaseline />
+        <SnackbarContext.Provider value={snackbarContext}>
-        <main>
+          <CssBaseline />
-          <Typography variant="h2" component="h1" align="center" gutterBottom>
+          <main style={{ maxHeight: 'calc(100vh - 70px)', overflowY: 'auto' }}>
-            Solve your ADF Problem with OBDDs!
+            <RouterProvider router={browserRouter} />
-          </Typography>
+          </main>
+          <Footer />
 
-          <Container>
+          <Backdrop
-            <TextField
+            open={loading}
-              name="code"
+          >
-              label="Put your code here:"
+            <CircularProgress color="inherit" />
-              helperText={(
+          </Backdrop>
-                <>
+          <Snackbar
-                  For more info on the syntax, have a
+            open={!!snackbarInfo}
-                  look
+            autoHideDuration={10000}
-                  {' '}
+            onClose={() => setSnackbarInfo(undefined)}
-                  <Link href="https://github.com/ellmau/adf-obdd" target="_blank" rel="noreferrer">here</Link>
+          >
-                  .
+            <Alert severity={snackbarInfo?.severity}>{snackbarInfo?.message}</Alert>
-                </>
+          </Snackbar>
-              )}
+        </SnackbarContext.Provider>
-              multiline
-              fullWidth
-              variant="filled"
-              value={code}
-              onChange={(event) => { setCode(event.target.value); }}
-            />
-          </Container>
-          <Container sx={{ marginTop: 2, marginBottom: 2 }}>
-            <FormControl>
-              <FormLabel id="parsing-radio-group">Parsing Strategy</FormLabel>
-              <RadioGroup
-                row
-                aria-labelledby="parsing-radio-group"
-                name="parsing"
-                value={parsing}
-                onChange={(e) => setParsing(((e.target as HTMLInputElement).value) as Parsing)}
-              >
-                <FormControlLabel value={Parsing.Naive} control={<Radio />} label="Naive" />
-                <FormControlLabel value={Parsing.Hybrid} control={<Radio />} label="Hybrid" />
-              </RadioGroup>
-            </FormControl>
-            <br />
-            <br />
-            <Button variant="outlined" onClick={() => submitHandler(Strategy.ParseOnly)}>Parse only</Button>
-            {' '}
-            <Button variant="outlined" onClick={() => submitHandler(Strategy.Ground)}>Grounded Model</Button>
-            {' '}
-            <Button variant="outlined" onClick={() => submitHandler(Strategy.Complete)}>Complete Models</Button>
-            {' '}
-            <Button variant="outlined" onClick={() => submitHandler(Strategy.Stable)}>Stable Models (naive heuristics)</Button>
-            {' '}
-            <Button disabled={parsing !== Parsing.Hybrid} variant="outlined" onClick={() => submitHandler(Strategy.StableCountingA)}>Stable Models (counting heuristic A)</Button>
-            {' '}
-            <Button disabled={parsing !== Parsing.Hybrid} variant="outlined" onClick={() => submitHandler(Strategy.StableCountingB)}>Stable Models (counting heuristic B)</Button>
-            {' '}
-            <Button variant="outlined" onClick={() => submitHandler(Strategy.StableNogood)}>Stable Models using nogoods (Simple Heuristic)</Button>
-          </Container>
-
-          {graphs
-          && (
-          <Container sx={{ marginTop: 4, marginBottom: 4 }}>
-            {graphs.length > 1
-              && (
-              <>
-                Models:
-                <br />
-                <Pagination variant="outlined" shape="rounded" count={graphs.length} page={graphIndex + 1} onChange={(e, value) => setGraphIndex(value - 1)} />
-              </>
-              )}
-            {graphs.length > 0
-              && (
-              <Paper elevation={3} square sx={{ marginTop: 4, marginBottom: 4 }}>
-                <GraphG6 graph={graphs[graphIndex]} />
-              </Paper>
-              )}
-            {graphs.length === 0
-              && <>No models!</>}
-          </Container>
-          )}
-        </main>
-        <Footer />
-
-        <Backdrop
-          open={loading}
-        >
-          <CircularProgress color="inherit" />
-        </Backdrop>
       </LoadingContext.Provider>
     </ThemeProvider>
   );

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) {
       </DialogContent>
       <DialogActions>
         <Button type="button" onClick={() => close()}>Cancel</Button>
-        <Button type="submit">{formType}</Button>
+        <Button type="submit" variant="contained" color="success">{formType}</Button>
         {formType === UserFormType.Update
         // TODO: add another confirm dialog here
           && (
           <Button
             type="button"
             variant="outlined"
+            color="error"
             onClick={() => {
               // eslint-disable-next-line no-alert
               if (window.confirm('Are you sure that you want to delete your account?')) {
@@ -138,13 +139,12 @@ function UserForm({ username: propUsername, formType, close }: UserFormProps) {
 UserForm.defaultProps = { username: undefined };
 
 function Footer() {
+  const { status: snackbarInfo, setStatus: setSnackbarInfo } = useContext(SnackbarContext);
   const [username, setUsername] = useState<string>();
   const [tempUser, setTempUser] = useState<boolean>();
   const [dialogTypeOpen, setDialogTypeOpen] = useState<UserFormType | null>(null);
-  const [snackbarInfo, setSnackbarInfo] = useState<{
+
-    message: string,
+  const isFirstRender = useRef(true);
-    severity: AlertColor,
-  } | undefined>();
 
   const logout = useCallback(() => {
     fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/users/logout`, {
@@ -157,19 +157,22 @@ function Footer() {
       .then((res) => {
         switch (res.status) {
           case 200:
-            setSnackbarInfo({ message: 'Logout successful!', severity: 'success' });
+            setSnackbarInfo({ message: 'Logout successful!', severity: 'success', potentialUserChange: true });
             setUsername(undefined);
             break;
           default:
-            setSnackbarInfo({ message: 'An error occurred while trying to log out.', severity: 'error' });
+            setSnackbarInfo({ message: 'An error occurred while trying to log out.', severity: 'error', potentialUserChange: false });
             break;
         }
       });
   }, [setSnackbarInfo]);
 
   useEffect(() => {
-    // Intuition: If the dialog was just closed (or on first render).
+    // TODO: having the info if the user may have changed on the snackbar info
-    if (!dialogTypeOpen) {
+    // is a bit lazy and unclean; be better!
+    if (isFirstRender.current || snackbarInfo?.potentialUserChange) {
+      isFirstRender.current = false;
+
       fetch(`${process.env.NODE_ENV === 'development' ? '//localhost:8080' : ''}/users/info`, {
         method: 'GET',
         credentials: process.env.NODE_ENV === 'development' ? 'include' : 'same-origin',
@@ -191,7 +194,7 @@ function Footer() {
           }
         });
     }
-  }, [dialogTypeOpen]);
+  }, [snackbarInfo?.potentialUserChange]);
 
   return (
     <>
@@ -222,18 +225,13 @@ function Footer() {
           formType={dialogTypeOpen}
           close={(message, severity) => {
             setDialogTypeOpen(null);
-            setSnackbarInfo((!!message && !!severity) ? { message, severity } : undefined);
+            setSnackbarInfo((!!message && !!severity)
+              ? { message, severity, potentialUserChange: true }
+              : undefined);
           }}
           username={dialogTypeOpen === UserFormType.Update ? username : undefined}
         />
       </Dialog>
-      <Snackbar
-        open={!!snackbarInfo}
-        autoHideDuration={10000}
-        onClose={() => setSnackbarInfo(undefined)}
-      >
-        <Alert severity={snackbarInfo?.severity}>{snackbarInfo?.message}</Alert>
-      </Snackbar>
     </>
   );
 }

frontend/src/components/graph-g6.tsx

@@ -183,7 +183,7 @@ function GraphG6(props: Props) {
         graphRef.current = new Graph({
           container: ref.current!,
           width: 1200,
-          height: 600,
+          height: 400,
           fitView: true,
           modes: {
             default: ['drag-canvas', 'zoom-canvas', 'drag-node'],
@@ -368,7 +368,9 @@ function GraphG6(props: Props) {
       <div style={{ padding: 4 }}>
         <span style={{ color: '#ed6c02', marginRight: 8 }}>lo edge (condition is false)</span>
         {' '}
-        <span style={{ color: '#1976d2' }}>hi edge (condition is true)</span>
+        <span style={{ color: '#1976d2', marginRight: 8 }}>hi edge (condition is true)</span>
+        {' '}
+        Click nodes to hightlight paths! (You can also drag and zoom.)
       </div>
     </>
   );

frontend/src/components/snackbar-context.ts

@@ -0,0 +1,17 @@
+import { createContext } from 'react';
+
+import { AlertColor } from '@mui/material';
+
+type Status = { message: string, severity: AlertColor, potentialUserChange: boolean } | undefined;
+
+interface ISnackbarContext {
+  status: Status;
+  setStatus: (status: Status) => void;
+}
+
+const SnackbarContext = createContext<ISnackbarContext>({
+  status: undefined,
+  setStatus: () => {},
+});
+
+export default SnackbarContext;

frontend/yarn.lock

@@ -1296,6 +1296,11 @@
   dependencies:
     "@babel/runtime" "^7.0.0"
 
+"@remix-run/router@1.5.0":
+  version "1.5.0"
+  resolved "https://registry.yarnpkg.com/@remix-run/router/-/router-1.5.0.tgz#57618e57942a5f0131374a9fdb0167e25a117fdc"
+  integrity sha512-bkUDCp8o1MvFO+qxkODcbhSqRa6P2GXgrGZVpt0dCXNW2HCSCqYI0ZoAqEOSAjRWmmlKcYgFvN4B4S+zo/f8kg==
+
 "@swc/helpers@^0.4.12":
   version "0.4.14"
   resolved "https://registry.yarnpkg.com/@swc/helpers/-/helpers-0.4.14.tgz#1352ac6d95e3617ccb7c1498ff019654f1e12a74"
@@ -3615,6 +3620,21 @@ react-refresh@^0.9.0:
   resolved "https://registry.yarnpkg.com/react-refresh/-/react-refresh-0.9.0.tgz#71863337adc3e5c2f8a6bfddd12ae3bfe32aafbf"
   integrity sha512-Gvzk7OZpiqKSkxsQvO/mbTN1poglhmAV7gR/DdIrRrSMXraRQQlfikRJOr3Nb9GTMPC5kof948Zy6jJZIFtDvQ==
 
+react-router-dom@^6.10.0:
+  version "6.10.0"
+  resolved "https://registry.yarnpkg.com/react-router-dom/-/react-router-dom-6.10.0.tgz#090ddc5c84dc41b583ce08468c4007c84245f61f"
+  integrity sha512-E5dfxRPuXKJqzwSe/qGcqdwa18QiWC6f3H3cWXM24qj4N0/beCIf/CWTipop2xm7mR0RCS99NnaqPNjHtrAzCg==
+  dependencies:
+    "@remix-run/router" "1.5.0"
+    react-router "6.10.0"
+
+react-router@6.10.0:
+  version "6.10.0"
+  resolved "https://registry.yarnpkg.com/react-router/-/react-router-6.10.0.tgz#230f824fde9dd0270781b5cb497912de32c0a971"
+  integrity sha512-Nrg0BWpQqrC3ZFFkyewrflCud9dio9ME3ojHCF/WLsprJVzkq3q3UeEhMCAW1dobjeGbWgjNn/PVF6m46ANxXQ==
+  dependencies:
+    "@remix-run/router" "1.5.0"
+
 react-transition-group@^4.4.5:
   version "4.4.5"
   resolved "https://registry.yarnpkg.com/react-transition-group/-/react-transition-group-4.4.5.tgz#e53d4e3f3344da8521489fbef8f2581d42becdd1"

server/Cargo.toml

@@ -25,6 +25,7 @@ argon2 = "0.5.0"
 actix-session = { version="0.7.2", features = ["cookie-session"] }
 names = "0.14.0"
 futures-util = "0.3.28"
+actix-multipart = "0.6.0"
 
 [features]
 cors_for_local_development = []

server/docker-compose.yml

@@ -0,0 +1,24 @@
+version: '3.1'
+
+services:
+
+  mongo:
+    image: mongo
+    restart: always
+    ports:
+      - 27017:27017
+    environment:
+      MONGO_INITDB_ROOT_USERNAME: root
+      MONGO_INITDB_ROOT_PASSWORD: example
+    volumes:
+      - ./mongodb-data:/data/db
+
+  mongo-express:
+    image: mongo-express
+    restart: always
+    ports:
+      - 8081:8081
+    environment:
+      ME_CONFIG_MONGODB_ADMINUSERNAME: root
+      ME_CONFIG_MONGODB_ADMINPASSWORD: example
+      ME_CONFIG_MONGODB_URL: mongodb://root:example@mongo:27017/

server/src/adf.rs

@@ -4,6 +4,7 @@ use std::sync::{Arc, RwLock};
 use std::time::Duration;
 
 use actix_identity::Identity;
+use actix_multipart::form::{tempfile::TempFile, text::Text, MultipartForm};
 use actix_web::rt::spawn;
 use actix_web::rt::task::spawn_blocking;
 use actix_web::rt::time::timeout;
@@ -27,13 +28,13 @@ use crate::user::{username_exists, User};
 type Ac = Vec<Term>;
 type AcDb = Vec<String>;
 
-#[derive(Copy, Clone, Deserialize, Serialize)]
+#[derive(Copy, Clone, Debug, Deserialize, Serialize)]
 pub(crate) enum Parsing {
     Naive,
     Hybrid,
 }
 
-#[derive(Copy, Clone, PartialEq, Eq, Hash, Deserialize, Serialize)]
+#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Deserialize, Serialize)]
 pub(crate) enum Strategy {
     Ground,
     Complete,
@@ -56,6 +57,7 @@ impl From<AcAndGraph> for Bson {
 }
 
 #[derive(Clone, Default, Deserialize, Serialize)]
+#[serde(tag = "type", content = "content")]
 pub(crate) enum OptionWithError<T> {
     Some(T),
     Error(String),
@@ -182,11 +184,36 @@ pub(crate) struct AdfProblem {
     pub(crate) acs_per_strategy: AcsPerStrategy,
 }
 
-#[derive(Clone, Deserialize)]
+#[derive(MultipartForm)]
-struct AddAdfProblemBody {
+struct AddAdfProblemBodyMultipart {
-    name: Option<String>,
+    name: Text<String>,
+    code: Option<Text<String>>, // Either Code or File is set
+    file: Option<TempFile>,     // Either Code or File is set
+    parsing: Text<Parsing>,
+}
+
+#[derive(Clone)]
+struct AddAdfProblemBodyPlain {
+    name: String,
     code: String,
-    parse_strategy: Parsing,
+    parsing: Parsing,
+}
+
+impl TryFrom<AddAdfProblemBodyMultipart> for AddAdfProblemBodyPlain {
+    type Error = &'static str;
+
+    fn try_from(source: AddAdfProblemBodyMultipart) -> Result<Self, Self::Error> {
+        Ok(Self {
+            name: source.name.into_inner(),
+            code: source
+                .file
+                .map(|f| std::io::read_to_string(f.file).expect("TempFile should be readable"))
+                .or_else(|| source.code.map(|c| c.into_inner()))
+                .and_then(|code| (!code.is_empty()).then_some(code))
+                .ok_or("Either a file or the code has to be provided.")?,
+            parsing: source.parsing.into_inner(),
+        })
+    }
 }
 
 async fn adf_problem_exists(
@@ -233,9 +260,12 @@ async fn add_adf_problem(
     req: HttpRequest,
     app_state: web::Data<AppState>,
     identity: Option<Identity>,
-    req_body: web::Json<AddAdfProblemBody>,
+    req_body: MultipartForm<AddAdfProblemBodyMultipart>,
 ) -> impl Responder {
-    let adf_problem_input: AddAdfProblemBody = req_body.into_inner();
+    let adf_problem_input: AddAdfProblemBodyPlain = match req_body.into_inner().try_into() {
+        Ok(input) => input,
+        Err(err) => return HttpResponse::BadRequest().body(err),
+    };
     let adf_coll: mongodb::Collection<AdfProblem> = app_state
         .mongodb_client
         .database(DB_NAME)
@@ -291,35 +321,32 @@ async fn add_adf_problem(
         Some(Ok(username)) => username,
     };
 
-    let problem_name = match &adf_problem_input.name {
+    let problem_name = if !adf_problem_input.name.is_empty() {
-        Some(name) => {
+        if adf_problem_exists(&adf_coll, &adf_problem_input.name, &username).await {
-            if adf_problem_exists(&adf_coll, name, &username).await {
+            return HttpResponse::Conflict()
-                return HttpResponse::Conflict()
+                .body("ADF Problem with that name already exists. Please pick another one!");
-                    .body("ADF Problem with that name already exists. Please pick another one!");
-            }
-
-            name.clone()
         }
-        None => {
-            let gen = Generator::with_naming(Name::Numbered);
-            let candidates = gen.take(10);
 
-            let mut name: Option<String> = None;
+        adf_problem_input.name.clone()
-            for candidate in candidates {
+    } else {
-                if name.is_some() {
+        let gen = Generator::with_naming(Name::Numbered);
-                    continue;
+        let candidates = gen.take(10);
-                }
 
-                if !(adf_problem_exists(&adf_coll, &candidate, &username).await) {
+        let mut name: Option<String> = None;
-                    name = Some(candidate);
+        for candidate in candidates {
-                }
+            if name.is_some() {
+                continue;
             }
 
-            match name {
+            if !(adf_problem_exists(&adf_coll, &candidate, &username).await) {
-                Some(name) => name,
+                name = Some(candidate);
-                None => {
+            }
-                    return HttpResponse::InternalServerError().body("Could not generate new name.")
+        }
-                }
+
+        match name {
+            Some(name) => name,
+            None => {
+                return HttpResponse::InternalServerError().body("Could not generate new name.")
             }
         }
     };
@@ -328,7 +355,7 @@ async fn add_adf_problem(
         name: problem_name.clone(),
         username: username.clone(),
         code: adf_problem_input.code.clone(),
-        parsing_used: adf_problem_input.parse_strategy,
+        parsing_used: adf_problem_input.parsing,
         adf: SimplifiedAdfOpt::None,
         acs_per_strategy: AcsPerStrategy::default(),
     };
@@ -362,21 +389,25 @@ async fn add_adf_problem(
             std::thread::sleep(Duration::from_secs(20));
 
             let parser = AdfParser::default();
-            parser.parse()(&adf_problem_input.code)
+            let parse_result = parser.parse()(&adf_problem_input.code)
-                .map_err(|_| "ADF could not be parsed, double check your input!")?;
+                .map_err(|_| "ADF could not be parsed, double check your input!");
 
-            let lib_adf = match adf_problem_input.parse_strategy {
+            let result = parse_result.map(|_| {
-                Parsing::Naive => Adf::from_parser(&parser),
+                let lib_adf = match adf_problem_input.parsing {
-                Parsing::Hybrid => {
+                    Parsing::Naive => Adf::from_parser(&parser),
-                    let bd_adf = BdAdf::from_parser(&parser);
+                    Parsing::Hybrid => {
-                    bd_adf.hybrid_step_opt(false)
+                        let bd_adf = BdAdf::from_parser(&parser);
-                }
+                        bd_adf.hybrid_step_opt(false)
-            };
+                    }
+                };
 
-            let ac_and_graph = AcAndGraph {
+                let ac_and_graph = AcAndGraph {
-                ac: lib_adf.ac.iter().map(|t| t.0.to_string()).collect(),
+                    ac: lib_adf.ac.iter().map(|t| t.0.to_string()).collect(),
-                graph: lib_adf.into_double_labeled_graph(None),
+                    graph: lib_adf.into_double_labeled_graph(None),
-            };
+                };
+
+                (SimplifiedAdf::from_lib_adf(lib_adf), ac_and_graph)
+            });
 
             app_state
                 .currently_running
@@ -384,7 +415,7 @@ async fn add_adf_problem(
                 .unwrap()
                 .remove(&running_info);
 
-            Ok::<_, &str>((SimplifiedAdf::from_lib_adf(lib_adf), ac_and_graph))
+            result
         }),
     );
 
@@ -484,24 +515,30 @@ async fn solve_adf_problem(
         Strategy::StableNogood => adf_problem.acs_per_strategy.stable_nogood.is_some(),
     };
 
+    let username_clone = username.clone();
+    let problem_name_clone = problem_name.clone();
+
+    let running_info = RunningInfo {
+        username: username_clone,
+        adf_name: problem_name_clone,
+        task: Task::Solve(adf_problem_input.strategy),
+    };
+
     // NOTE: we could also return the result here instead of throwing an error but I think the canonical way should just be to call the get endpoint for the problem.
-    if has_been_solved {
+    if has_been_solved
+        || app_state
+            .currently_running
+            .lock()
+            .unwrap()
+            .contains(&running_info)
+    {
         return HttpResponse::Conflict()
             .body("The ADF problem has already been solved with this strategy. You can just get the solution from the problem data directly.");
     }
 
-    let username_clone = username.clone();
-    let problem_name_clone = problem_name.clone();
-
     let acs_and_graphs_fut = timeout(
         COMPUTE_TIME,
         spawn_blocking(move || {
-            let running_info = RunningInfo {
-                username: username_clone,
-                adf_name: problem_name_clone,
-                task: Task::Solve(adf_problem_input.strategy),
-            };
-
             app_state
                 .currently_running
                 .lock()

server/src/config.rs

@@ -17,13 +17,14 @@ pub(crate) const DB_NAME: &str = "adf-obdd";
 pub(crate) const USER_COLL: &str = "users";
 pub(crate) const ADF_COLL: &str = "adf-problems";
 
-#[derive(Copy, Clone, PartialEq, Eq, Hash, Serialize)]
+#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Serialize)]
+#[serde(tag = "type", content = "content")]
 pub(crate) enum Task {
     Parse,
     Solve(Strategy),
 }
 
-#[derive(Clone, PartialEq, Eq, Hash)]
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
 pub(crate) struct RunningInfo {
     pub(crate) username: String,
     pub(crate) adf_name: String,

server/src/main.rs

@@ -43,6 +43,12 @@ async fn main() -> std::io::Result<()> {
     // cookie secret ket
     let secret_key = Key::generate();
 
+    // needs to be set outside of httpserver closure to only create it once!
+    let app_data = web::Data::new(AppState {
+        mongodb_client: client.clone(),
+        currently_running: Mutex::new(HashSet::new()),
+    });
+
     HttpServer::new(move || {
         let app = App::new();
 
@@ -62,37 +68,34 @@ async fn main() -> std::io::Result<()> {
         #[cfg(not(feature = "cors_for_local_development"))]
         let cookie_secure = true;
 
-        app.app_data(web::Data::new(AppState {
+        app.app_data(app_data.clone())
-            mongodb_client: client.clone(),
+            .wrap(IdentityMiddleware::default())
-            currently_running: Mutex::new(HashSet::new()),
+            .wrap(
-        }))
+                SessionMiddleware::builder(CookieSessionStore::default(), secret_key.clone())
-        .wrap(IdentityMiddleware::default())
+                    .cookie_name("adf-obdd-service-auth".to_owned())
-        .wrap(
+                    .cookie_secure(cookie_secure)
-            SessionMiddleware::builder(CookieSessionStore::default(), secret_key.clone())
+                    .session_lifecycle(PersistentSession::default().session_ttl(COOKIE_DURATION))
-                .cookie_name("adf-obdd-service-auth".to_owned())
+                    .build(),
-                .cookie_secure(cookie_secure)
+            )
-                .session_lifecycle(PersistentSession::default().session_ttl(COOKIE_DURATION))
+            .service(
-                .build(),
+                web::scope("/users")
-        )
+                    .service(register)
-        .service(
+                    .service(delete_account)
-            web::scope("/users")
+                    .service(login)
-                .service(register)
+                    .service(logout)
-                .service(delete_account)
+                    .service(user_info)
-                .service(login)
+                    .service(update_user),
-                .service(logout)
+            )
-                .service(user_info)
+            .service(
-                .service(update_user),
+                web::scope("/adf")
-        )
+                    .service(add_adf_problem)
-        .service(
+                    .service(solve_adf_problem)
-            web::scope("/adf")
+                    .service(get_adf_problem)
-                .service(add_adf_problem)
+                    .service(delete_adf_problem)
-                .service(solve_adf_problem)
+                    .service(get_adf_problems_for_user),
-                .service(get_adf_problem)
+            )
-                .service(delete_adf_problem)
+            // this mus be last to not override anything
-                .service(get_adf_problems_for_user),
+            .service(fs::Files::new("/", ASSET_DIRECTORY).index_file("index.html"))
-        )
-        // this mus be last to not override anything
-        .service(fs::Files::new("/", ASSET_DIRECTORY).index_file("index.html"))
     })
     .bind(("0.0.0.0", 8080))?
     .run()

server/src/user.rs

@@ -110,39 +110,44 @@ async fn delete_account(
         .database(DB_NAME)
         .collection(ADF_COLL);
 
-    match identity.map(|id| id.id()) {
+    match identity {
-        None => HttpResponse::Unauthorized().body("You need to login to delete your account."),
+        None => HttpResponse::Unauthorized().body("You are not logged in."),
-        Some(Err(err)) => HttpResponse::InternalServerError().body(err.to_string()),
+        Some(id) => match id.id() {
-        Some(Ok(username)) => {
+            Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
-            // Delete all adfs created by user
+            Ok(username) => {
-            match adf_coll
+                // Delete all adfs created by user
-                .delete_many(doc! { "username": &username }, None)
+                match adf_coll
-                .await
+                    .delete_many(doc! { "username": &username }, None)
-            {
+                    .await
-                Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
+                {
-                Ok(DeleteResult {
+                    Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
-                    deleted_count: _, ..
+                    Ok(DeleteResult {
-                }) => {
+                        deleted_count: _, ..
-                    // Delete actual user
+                    }) => {
-                    match user_coll
+                        // Delete actual user
-                        .delete_one(doc! { "username": &username }, None)
+                        match user_coll
-                        .await
+                            .delete_one(doc! { "username": &username }, None)
-                    {
+                            .await
-                        Ok(DeleteResult {
+                        {
-                            deleted_count: 0, ..
+                            Ok(DeleteResult {
-                        }) => HttpResponse::InternalServerError()
+                                deleted_count: 0, ..
-                            .body("Account could not be deleted."),
+                            }) => HttpResponse::InternalServerError()
-                        Ok(DeleteResult {
+                                .body("Account could not be deleted."),
-                            deleted_count: 1, ..
+                            Ok(DeleteResult {
-                        }) => HttpResponse::Ok().body("Account deleted."),
+                                deleted_count: 1, ..
-                        Ok(_) => unreachable!(
+                            }) => {
+                                id.logout();
+                                HttpResponse::Ok().body("Account deleted.")
+                            }
+                            Ok(_) => unreachable!(
                             "delete_one removes at most one entry so all cases are covered already"
                         ),
-                        Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
+                            Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
+                        }
                     }
                 }
             }
-        }
+        },
     }
 }
 
@@ -237,28 +242,33 @@ async fn user_info(app_state: web::Data<AppState>, identity: Option<Identity>) -
         .database(DB_NAME)
         .collection(USER_COLL);
 
-    match identity.map(|id| id.id()) {
+    match identity {
         None => {
             HttpResponse::Unauthorized().body("You need to login get your account information.")
         }
-        Some(Err(err)) => HttpResponse::InternalServerError().body(err.to_string()),
+        Some(id) => match id.id() {
-        Some(Ok(username)) => {
+            Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
-            match user_coll
+            Ok(username) => {
-                .find_one(doc! { "username": &username }, None)
+                match user_coll
-                .await
+                    .find_one(doc! { "username": &username }, None)
-            {
+                    .await
-                Ok(Some(user)) => {
+                {
-                    let info = UserInfo {
+                    Ok(Some(user)) => {
-                        username: user.username,
+                        let info = UserInfo {
-                        temp: user.password.is_none(),
+                            username: user.username,
-                    };
+                            temp: user.password.is_none(),
+                        };
 
-                    HttpResponse::Ok().json(info)
+                        HttpResponse::Ok().json(info)
+                    }
+                    Ok(None) => {
+                        id.logout();
+                        HttpResponse::NotFound().body("Logged in user does not exist anymore.")
+                    }
+                    Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
                 }
-                Ok(None) => HttpResponse::NotFound().body("Logged in user does not exist anymore."),
-                Err(err) => HttpResponse::InternalServerError().body(err.to_string()),
             }
-        }
+        },
     }
 }