WIP: build frontend for ADFs

.dockerignore

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

Dockerfile

@@ -1,5 +1,5 @@
 # 1. BUILD-CONTAINER: Frontend
-FROM node:hydrogen-alpine
+FROM node:gallium-alpine
 
 WORKDIR /root
 
@@ -30,7 +30,5 @@ 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/src/components/adf-details.tsx

@@ -1,33 +1,14 @@
-import React, {
+import React from '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 {AlertColor} from '@mui/material';
-import LoadingContext from './loading-context';
+
-import SnackbarContext from './snackbar-context';
+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 const STRATEGIES_WITHOUT_PARSE: StrategyCamelCase[] = ['Ground', 'Complete', 'Stable', 'StableCountingA', 'StableCountingB', 'StableNogood'];
 
 export interface AcAndGraph {
   ac: string[],
@@ -55,8 +36,7 @@ export interface AdfProblemInfo {
   name: string,
   code: string,
   parsing_used: Parsing,
-  // NOTE: the keys are really only strategies
+  acs_per_strategy: { [key in StrategySnakeCase]: AcsWithGraphsOpt }, // NOTE: the keys are really only strategies
-  acs_per_strategy: { [key in StrategySnakeCase]: AcsWithGraphsOpt },
   running_tasks: Task[],
 }
 
@@ -66,11 +46,9 @@ export function acsWithGraphOptToColor(status: AcsWithGraphsOpt, running: boolea
   }
 
   switch (status.type) {
-    case 'None': return 'info';
+      case 'None': return 'info';
-    case 'Error': return 'error';
+      case 'Error': return 'error';
-    case 'Some': return 'success';
+      case 'Some': return 'success';
-    default:
-      throw new Error('Unknown type union variant (cannot occur)');
   }
 }
 
@@ -80,261 +58,15 @@ export function acsWithGraphOptToText(status: AcsWithGraphsOpt, running: boolean
   }
 
   switch (status.type) {
-    case 'None': return 'Not attempted';
+      case 'None': return 'Not attempted';
-    case 'Error': return 'Failed';
+      case 'Error': return 'Failed';
-    case 'Some': return 'Done';
+      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 (
-    <>
+    <div>Details</div>
-      <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>
-    </>
   );
 }
 

frontend/src/components/adf-new-form.tsx

@@ -3,12 +3,16 @@ import React, {
 } from 'react';
 
 import {
+  Backdrop,
   Button,
+  CircularProgress,
+  CssBaseline,
   Container,
   FormControl,
   FormControlLabel,
   FormLabel,
   Link,
+  Pagination,
   Paper,
   Radio,
   RadioGroup,
@@ -33,7 +37,7 @@ ac(b,b).
 ac(c,and(a,b)).
 ac(d,neg(b)).`;
 
-function AdfNewForm({ fetchProblems }: { fetchProblems: () => void; }) {
+function AdfNewForm({fetchProblems}: { fetchProblems: () => void; }) {
   const { setLoading } = useContext(LoadingContext);
   const { setStatus: setSnackbarInfo } = useContext(SnackbarContext);
   const [isFileUpload, setFileUpload] = useState(false);
@@ -50,10 +54,7 @@ function AdfNewForm({ fetchProblems }: { fetchProblems: () => void; }) {
       const formData = new FormData();
 
       if (isFileUpload && fileRef.current) {
-        const file = fileRef.current.files?.[0];
+        formData.append('file', fileRef.current.files![0]);
-        if (file) {
-          formData.append('file', file);
-        }
       } else {
         formData.append('code', code);
       }
@@ -84,84 +85,84 @@ function AdfNewForm({ fetchProblems }: { fetchProblems: () => void; }) {
 
   return (
     <Container>
-      <Paper elevation={8} sx={{ padding: 2 }}>
+    <Paper elevation={8} sx={{ padding: 2 }}>
-        <Typography variant="h4" component="h2" align="center" gutterBottom>
+      <Typography variant="h4" component="h2" align="center" gutterBottom>
-          Add a new Problem
+        Add a new Problem
-        </Typography>
+      </Typography>
-        <Container sx={{ marginTop: 2, marginBottom: 2 }}>
+      <Container sx={{ marginTop: 2, marginBottom: 2 }}>
-          <Stack direction="row" justifyContent="center">
+      <Stack direction="row" justifyContent="center">
-            <ToggleButtonGroup
+      <ToggleButtonGroup
-              value={isFileUpload}
+        value={isFileUpload}
-              exclusive
+        exclusive
-              onChange={(_e, newValue) => { setFileUpload(newValue); setFilename(''); }}
+    onChange={(_e, newValue) => { setFileUpload(newValue); setFilename(''); }}
-            >
+      >
-              <ToggleButton value={false}>
+        <ToggleButton value={false}>
-                Write by Hand
+          Write by Hand
-              </ToggleButton>
+        </ToggleButton>
-              <ToggleButton value>
+        <ToggleButton value>
-                Upload File
+          Upload File
-              </ToggleButton>
+        </ToggleButton>
-            </ToggleButtonGroup>
+      </ToggleButtonGroup>
-          </Stack>
+      </Stack>
-        </Container>
+      </Container>
 
         <Container sx={{ marginTop: 2, marginBottom: 2 }}>
-          {isFileUpload ? (
+      {isFileUpload ? (
-            <Stack direction="row" justifyContent="center">
+      <Stack direction="row" justifyContent="center">
-              <Button component="label">
+        <Button component="label">
-                {(!!filename && fileRef?.current?.files?.[0]) ? `File '${filename.split(/[\\/]/).pop()}' selected! (Click to change)` : 'Upload File'}
+          {(!!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} />
+          <input hidden type="file" onChange={(event) => { setFilename(event.target.value); }} ref={fileRef} />
-              </Button>
+        </Button>
-            </Stack>
+          </Stack>
-          ) : (
+      ) : (
-            <TextField
+          <TextField
-              name="code"
+            name="code"
-              label="Put your code here:"
+            label="Put your code here:"
-              helperText={(
+            helperText={(
-                <>
+              <>
-                  For more info on the syntax, have a
+                For more info on the syntax, have a
-                  look
+                look
-                  {' '}
+                {' '}
-                  <Link href="https://github.com/ellmau/adf-obdd" target="_blank" rel="noreferrer">here</Link>
+                <Link href="https://github.com/ellmau/adf-obdd" target="_blank" rel="noreferrer">here</Link>
-                  .
+                .
-                </>
+              </>
               )}
-              multiline
+            multiline
-              fullWidth
+            fullWidth
-              variant="filled"
+            variant="filled"
-              value={code}
+            value={code}
-              onChange={(event) => { setCode(event.target.value); }}
+            onChange={(event) => { setCode(event.target.value); }}
-            />
+          />
-          )}
+      )}
         </Container>
 
-        <Container sx={{ marginTop: 2 }}>
+      <Container sx={{ marginTop: 2 }}>
-          <Stack direction="row" justifyContent="center" spacing={2}>
+      <Stack direction="row" justifyContent="center" spacing={2}>
-            <FormControl>
+      <FormControl>
-              <FormLabel id="parsing-radio-group">Parsing Strategy</FormLabel>
+        <FormLabel id="parsing-radio-group">Parsing Strategy</FormLabel>
-              <RadioGroup
+        <RadioGroup
-                row
+          row
-                aria-labelledby="parsing-radio-group"
+          aria-labelledby="parsing-radio-group"
-                name="parsing"
+          name="parsing"
-                value={parsing}
+          value={parsing}
-                onChange={(e) => setParsing(((e.target as HTMLInputElement).value) as Parsing)}
+          onChange={(e) => setParsing(((e.target as HTMLInputElement).value) as Parsing)}
-              >
+        >
-                <FormControlLabel value="Naive" control={<Radio />} label="Naive" />
+          <FormControlLabel value={'Naive'} control={<Radio />} label="Naive" />
-                <FormControlLabel value="Hybrid" control={<Radio />} label="Hybrid" />
+          <FormControlLabel value={'Hybrid'} control={<Radio />} label="Hybrid" />
-              </RadioGroup>
+        </RadioGroup>
-            </FormControl>
+      </FormControl>
-            <TextField
+      <TextField
-              name="name"
+        name="name"
-              label="Adf Problem Name (optional):"
+        label="Adf Problem Name (optional):"
-              variant="standard"
+        variant="standard"
-              value={name}
+        value={name}
-              onChange={(event) => { setName(event.target.value); }}
+        onChange={(event) => { setName(event.target.value); }}
-            />
+      />
-            <Button variant="outlined" onClick={() => addAdf()}>Add Adf Problem</Button>
+      <Button variant="outlined" onClick={() => addAdf()}>Add Adf Problem</Button>
-          </Stack>
+      </Stack>
-        </Container>
+      </Container>
-      </Paper>
+    </Paper>
-    </Container>
+      </Container>
   );
 }
 

frontend/src/components/adf-overview.tsx

@@ -1,15 +1,21 @@
-import React, {
+import React, { useState, useCallback, useEffect } from 'react';
-  useRef, useState, useCallback, useEffect, useContext,
-} from 'react';
-
-import {
-  useNavigate,
-} from 'react-router-dom';
 
 import {
+  Backdrop,
+  Button,
   Chip,
+  CircularProgress,
+  CssBaseline,
   Container,
+  FormControl,
+  FormControlLabel,
+  FormLabel,
+  Link,
+  Pagination,
   Paper,
+  Radio,
+  RadioGroup,
+  Stack,
   TableContainer,
   Table,
   TableHead,
@@ -17,29 +23,18 @@ import {
   TableCell,
   TableBody,
   Typography,
+  TextField,
+  ToggleButtonGroup,
+  ToggleButton,
 } from '@mui/material';
 
 import AdfNewForm from './adf-new-form';
 
-import {
+import {AdfProblemInfo, StrategySnakeCase, StrategyCamelCase, Task, acsWithGraphOptToColor, acsWithGraphOptToText} from './adf-details';
-  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/`, {
@@ -52,13 +47,10 @@ function AdfOverview() {
         .then((res) => {
           switch (res.status) {
             case 200:
-              res.json().then((resProblems) => {
+              res.json().then((problems) => {
-                setProblems(resProblems);
+                setProblems(problems);
               });
               break;
-            case 401:
-              setProblems([]);
-              break;
             default:
               break;
           }
@@ -68,72 +60,47 @@ function AdfOverview() {
   );
 
   useEffect(
-    () => {
+    () => { fetchProblems(); },
-      // 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(
+  // TODO set timeout for refetching if there are running problems
-    () => {
-      // 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
+      {problems.length > 0 &&
-        && (
         <Container sx={{ marginBottom: 4 }}>
-          <Paper elevation={8} sx={{ padding: 2 }}>
+      <Paper elevation={8} sx={{ padding: 2 }}>
-            <Typography variant="h4" component="h2" align="center" gutterBottom>
+      <Typography variant="h4" component="h2" align="center" gutterBottom>
-              Existing Problems
+        Existing Problems
-            </Typography>
+      </Typography>
-            <TableContainer component={Paper}>
+        <TableContainer component={Paper}>
-              <Table>
+          <Table>
-                <TableHead>
+        <TableHead>
-                  <TableRow>
+          <TableRow>
-                    <TableCell align="center">ADF Problem Name</TableCell>
+            <TableCell align="center">ADF Problem Name</TableCell>
-                    <TableCell align="center">Parse Status</TableCell>
+            <TableCell align="center">Parse Status</TableCell>
-                    <TableCell align="center">Grounded Solution</TableCell>
+            <TableCell align="center">Grounded Solution</TableCell>
-                    <TableCell align="center">Complete Solution</TableCell>
+            <TableCell align="center">Complete Solution</TableCell>
-                    <TableCell align="center">Stable Solution</TableCell>
+            <TableCell align="center">Stable Solution</TableCell>
-                    <TableCell align="center">Stable Solution (Counting Method A)</TableCell>
+            <TableCell align="center">Stable Solution (Counting Method A)</TableCell>
-                    <TableCell align="center">Stable Solution (Counting Method B)</TableCell>
+            <TableCell align="center">Stable Solution (Counting Method B)</TableCell>
-                    <TableCell align="center">Stable Solution (Nogood-Based)</TableCell>
+            <TableCell align="center">Stable Solution (Nogood-Based)</TableCell>
-                  </TableRow>
+          </TableRow>
-                </TableHead>
+        </TableHead>
-                <TableBody>
+        <TableBody>
-                  {problems.map((problem) => (
+          {problems.map((problem) => (
-                    <TableRow
+            <TableRow
-                      key={problem.name}
+              key={problem.name}
-                      onClick={() => { navigate(`/${problem.name}`); }}
+              sx={{ '&:last-child td, &:last-child th': { border: 0 } }}
-                      sx={{ '&:last-child td, &:last-child th': { border: 0 }, cursor: 'pointer' }}
+            >
-                    >
+              <TableCell component="th" scope="row">
-                      <TableCell component="th" scope="row">
+                {problem.name}
-                        {problem.name}
+              </TableCell>
-                      </TableCell>
+              {
-                      {
                 (() => {
                   const status = problem.acs_per_strategy.parse_only;
                   const running = problem.running_tasks.some((t: Task) => t.type === 'Parse');
@@ -141,30 +108,30 @@ function AdfOverview() {
                   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>;
+                  return <TableCell align="center"><Chip color={color} label={`${text} (${problem.parsing_used} Parsing)`} /></TableCell>;
                 })()
               }
-                      {
+              {
-                  STRATEGIES_WITHOUT_PARSE.map((strategy) => {
+                (['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 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 running = problem.running_tasks.some((t: Task) => t.type === 'Solve' && t.content === strategy);
 
-                    const color = acsWithGraphOptToColor(status, running);
+                  const color = acsWithGraphOptToColor(status, running);
-                    const text = acsWithGraphOptToText(status, running);
+                  const text = acsWithGraphOptToText(status, running);
 
-                    return <TableCell key={strategy} align="center"><Chip color={color} label={text} sx={{ cursor: 'inherit' }} /></TableCell>;
+                  return <TableCell align="center"><Chip color={color} label={text} /></TableCell>;
-                  })
+                })
               }
-                    </TableRow>
+            </TableRow>
-                  ))}
+          ))}
-                </TableBody>
+        </TableBody>
-              </Table>
+      </Table>
-            </TableContainer>
+        </TableContainer>
-          </Paper>
+      </Paper>
-        </Container>
+      </Container>
-        )}
+        }
-      <AdfNewForm fetchProblems={fetchProblems} />
+    <AdfNewForm fetchProblems={fetchProblems} />
-    </>
+      </>
   );
 }
 

frontend/src/components/app.tsx

@@ -1,4 +1,4 @@
-import React, { useState, useMemo } from 'react';
+import * as React from 'react';
 
 import { createBrowserRouter, RouterProvider } from 'react-router-dom';
 
@@ -7,18 +7,33 @@ import {
   Alert,
   AlertColor,
   Backdrop,
+  Button,
   CircularProgress,
   CssBaseline,
+  Container,
+  FormControl,
+  FormControlLabel,
+  FormLabel,
+  Link,
+  Pagination,
+  Paper,
+  Radio,
+  RadioGroup,
   Snackbar,
+  Typography,
+  TextField,
   useMediaQuery,
 } from '@mui/material';
 
 import LoadingContext from './loading-context';
 import SnackbarContext from './snackbar-context';
+import GraphG6, { GraphProps } from './graph-g6';
 import Footer from './footer';
 import AdfOverview from './adf-overview';
 import AdfDetails from './adf-details';
 
+const { useState, useCallback, useMemo } = React;
+
 const browserRouter = createBrowserRouter([
   {
     path: '/',
@@ -34,11 +49,12 @@ function App() {
   const prefersDarkMode = useMediaQuery('(prefers-color-scheme: dark)');
 
   const theme = useMemo(
-    () => createTheme({
+    () =>
-      palette: {
+      createTheme({
-        mode: prefersDarkMode ? 'dark' : 'light',
+        palette: {
-      },
+          mode: prefersDarkMode ? 'dark' : 'light',
-    }),
+        },
+      }),
     [prefersDarkMode],
   );
 
@@ -50,17 +66,14 @@ function App() {
     severity: AlertColor,
     potentialUserChange: boolean,
   } | undefined>();
-  const snackbarContext = useMemo(
+  const snackbarContext = useMemo(() => ({ status: snackbarInfo, setStatus: setSnackbarInfo }), [snackbarInfo, setSnackbarInfo]);
-    () => ({ status: snackbarInfo, setStatus: setSnackbarInfo }),
-    [snackbarInfo, setSnackbarInfo],
-  );
 
   return (
     <ThemeProvider theme={theme}>
       <LoadingContext.Provider value={loadingContext}>
         <SnackbarContext.Provider value={snackbarContext}>
           <CssBaseline />
-          <main style={{ maxHeight: 'calc(100vh - 70px)', overflowY: 'auto' }}>
+      <main style={{ maxHeight: 'calc(100vh - 70px)', overflowY: 'auto' }}>
             <RouterProvider router={browserRouter} />
           </main>
           <Footer />
@@ -83,4 +96,113 @@ function App() {
   );
 }
 
+// function BACKUP() {
+//   const [code, setCode] = useState(placeholder);
+//   const [parsing, setParsing] = useState(Parsing.Naive);
+//   const [graphs, setGraphs] = useState<GraphProps[]>();
+//   const [graphIndex, setGraphIndex] = useState(0);
+
+//   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],
+//   );
+
+//   return (<>
+//           <Typography variant="h2" component="h1" align="center" gutterBottom>
+//             Solve your ADF Problem with OBDDs!
+//           </Typography>
+
+//           <Container>
+//             <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, 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>
+//           )}
+//           </>
+//     );
+// }
+
 export default App;

frontend/src/components/footer.tsx

@@ -11,6 +11,7 @@ import {
   DialogActions,
   DialogContent,
   DialogTitle,
+  Snackbar,
   TextField,
   Toolbar,
 } from '@mui/material';
@@ -77,7 +78,7 @@ function UserForm({ username: propUsername, formType, close }: UserFormProps) {
         .then((res) => {
           switch (res.status) {
             case 200:
-              close(`Action '${del ? 'Delete' : formType}' successful!`, 'success');
+              close(`Action '${formType}' successful!`, 'success');
               break;
             default:
               setError(true);
@@ -113,14 +114,13 @@ function UserForm({ username: propUsername, formType, close }: UserFormProps) {
       </DialogContent>
       <DialogActions>
         <Button type="button" onClick={() => close()}>Cancel</Button>
-        <Button type="submit" variant="contained" color="success">{formType}</Button>
+        <Button type="submit">{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?')) {
@@ -157,7 +157,7 @@ function Footer() {
       .then((res) => {
         switch (res.status) {
           case 200:
-            setSnackbarInfo({ message: 'Logout successful!', severity: 'success', potentialUserChange: true });
+            setSnackbarInfo({ message: 'Logout successful!', severity: 'success', potentialUserChange: false });
             setUsername(undefined);
             break;
           default:
@@ -168,8 +168,7 @@ function Footer() {
   }, [setSnackbarInfo]);
 
   useEffect(() => {
-    // TODO: having the info if the user may have changed on the snackbar info
+    // TODO: having the info if the user may have changed on the snackbar info is a bit lazy and unclean; be better!
-    // is a bit lazy and unclean; be better!
     if (isFirstRender.current || snackbarInfo?.potentialUserChange) {
       isFirstRender.current = false;
 
@@ -225,9 +224,7 @@ function Footer() {
           formType={dialogTypeOpen}
           close={(message, severity) => {
             setDialogTypeOpen(null);
-            setSnackbarInfo((!!message && !!severity)
+            setSnackbarInfo((!!message && !!severity) ? { message, severity, potentialUserChange: true } : undefined);
-              ? { message, severity, potentialUserChange: true }
-              : undefined);
           }}
           username={dialogTypeOpen === UserFormType.Update ? username : undefined}
         />

frontend/src/components/graph-g6.tsx

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

server/docker-compose.yml

@@ -1,24 +0,0 @@
-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

@@ -28,13 +28,13 @@ use crate::user::{username_exists, User};
 type Ac = Vec<Term>;
 type AcDb = Vec<String>;
 
-#[derive(Copy, Clone, Debug, Deserialize, Serialize)]
+#[derive(Copy, Clone, Deserialize, Serialize)]
 pub(crate) enum Parsing {
     Naive,
     Hybrid,
 }
 
-#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Deserialize, Serialize)]
+#[derive(Copy, Clone, PartialEq, Eq, Hash, Deserialize, Serialize)]
 pub(crate) enum Strategy {
     Ground,
     Complete,
@@ -209,7 +209,6 @@ impl TryFrom<AddAdfProblemBodyMultipart> for AddAdfProblemBodyPlain {
                 .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(),
         })
@@ -389,25 +388,21 @@ async fn add_adf_problem(
             std::thread::sleep(Duration::from_secs(20));
 
             let parser = AdfParser::default();
-            let parse_result = parser.parse()(&adf_problem_input.code)
+            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 result = parse_result.map(|_| {
+            let lib_adf = match adf_problem_input.parsing {
-                let lib_adf = match adf_problem_input.parsing {
+                Parsing::Naive => Adf::from_parser(&parser),
-                    Parsing::Naive => Adf::from_parser(&parser),
+                Parsing::Hybrid => {
-                    Parsing::Hybrid => {
+                    let bd_adf = BdAdf::from_parser(&parser);
-                        let bd_adf = BdAdf::from_parser(&parser);
+                    bd_adf.hybrid_step_opt(false)
-                        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
@@ -415,7 +410,7 @@ async fn add_adf_problem(
                 .unwrap()
                 .remove(&running_info);
 
-            result
+            Ok::<_, &str>((SimplifiedAdf::from_lib_adf(lib_adf), ac_and_graph))
         }),
     );
 
@@ -515,30 +510,24 @@ 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,14 +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, Debug, PartialEq, Eq, Hash, Serialize)]
+#[derive(Copy, Clone, PartialEq, Eq, Hash, Serialize)]
 #[serde(tag = "type", content = "content")]
 pub(crate) enum Task {
     Parse,
     Solve(Strategy),
 }
 
-#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+#[derive(Clone, PartialEq, Eq, Hash)]
 pub(crate) struct RunningInfo {
     pub(crate) username: String,
     pub(crate) adf_name: String,

server/src/main.rs

@@ -43,12 +43,6 @@ 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();
 
@@ -68,34 +62,37 @@ async fn main() -> std::io::Result<()> {
         #[cfg(not(feature = "cors_for_local_development"))]
         let cookie_secure = true;
 
-        app.app_data(app_data.clone())
+        app.app_data(web::Data::new(AppState {
-            .wrap(IdentityMiddleware::default())
+            mongodb_client: client.clone(),
-            .wrap(
+            currently_running: Mutex::new(HashSet::new()),
-                SessionMiddleware::builder(CookieSessionStore::default(), secret_key.clone())
+        }))
-                    .cookie_name("adf-obdd-service-auth".to_owned())
+        .wrap(IdentityMiddleware::default())
-                    .cookie_secure(cookie_secure)
+        .wrap(
-                    .session_lifecycle(PersistentSession::default().session_ttl(COOKIE_DURATION))
+            SessionMiddleware::builder(CookieSessionStore::default(), secret_key.clone())
-                    .build(),
+                .cookie_name("adf-obdd-service-auth".to_owned())
-            )
+                .cookie_secure(cookie_secure)
-            .service(
+                .session_lifecycle(PersistentSession::default().session_ttl(COOKIE_DURATION))
-                web::scope("/users")
+                .build(),
-                    .service(register)
+        )
-                    .service(delete_account)
+        .service(
-                    .service(login)
+            web::scope("/users")
-                    .service(logout)
+                .service(register)
-                    .service(user_info)
+                .service(delete_account)
-                    .service(update_user),
+                .service(login)
-            )
+                .service(logout)
-            .service(
+                .service(user_info)
-                web::scope("/adf")
+                .service(update_user),
-                    .service(add_adf_problem)
+        )
-                    .service(solve_adf_problem)
+        .service(
-                    .service(get_adf_problem)
+            web::scope("/adf")
-                    .service(delete_adf_problem)
+                .service(add_adf_problem)
-                    .service(get_adf_problems_for_user),
+                .service(solve_adf_problem)
-            )
+                .service(get_adf_problem)
-            // this mus be last to not override anything
+                .service(delete_adf_problem)
-            .service(fs::Files::new("/", ASSET_DIRECTORY).index_file("index.html"))
+                .service(get_adf_problems_for_user),
+        )
+        // 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()