Add Detail View for ADF problems

frontend/src/components/adf-details.tsx

@@ -1,14 +1,33 @@
-import React from 'react';
+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 { AlertColor } from '@mui/material';
-
-import { GraphProps } from './graph-g6';
+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[],
@@ -70,8 +89,252 @@ export function acsWithGraphOptToText(status: AcsWithGraphsOpt, running: boolean
 }
 
 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-overview.tsx

@@ -2,6 +2,10 @@ import React, {
   useRef, useState, useCallback, useEffect, useContext,
 } from 'react';
 
+import {
+  useNavigate,
+} from 'react-router-dom';
+
 import {
   Chip,
   Container,
@@ -20,7 +24,7 @@ import AdfNewForm from './adf-new-form';
 import {
   AdfProblemInfo,
   StrategySnakeCase,
-  StrategyCamelCase,
+  STRATEGIES_WITHOUT_PARSE,
   Task,
   acsWithGraphOptToColor,
   acsWithGraphOptToText,
@@ -32,6 +36,8 @@ function AdfOverview() {
   const { status: snackbarInfo } = useContext(SnackbarContext);
   const [problems, setProblems] = useState<AdfProblemInfo[]>([]);
 
+  const navigate = useNavigate();
+
   const isFirstRender = useRef(true);
 
   const fetchProblems = useCallback(
@@ -121,7 +127,8 @@ function AdfOverview() {
                   {problems.map((problem) => (
                     <TableRow
                       key={problem.name}
-                      sx={{ '&:last-child td, &:last-child th': { border: 0 } }}
+                      onClick={() => { navigate(`/${problem.name}`); }}
+                      sx={{ '&:last-child td, &:last-child th': { border: 0 }, cursor: 'pointer' }}
                     >
                       <TableCell component="th" scope="row">
                         {problem.name}
@@ -134,19 +141,19 @@ 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)`} /></TableCell>;
+                  return <TableCell align="center"><Chip color={color} label={`${text} (${problem.parsing_used} Parsing)`} sx={{ cursor: 'inherit' }} /></TableCell>;
                 })()
               }
                       {
-                (['Ground', 'Complete', 'Stable', 'StableCountingA', 'StableCountingB', 'StableNogood'] as StrategyCamelCase[]).map((strategy) => {
-                  const status = problem.acs_per_strategy[strategy.replace(/^([A-Z])/, (_, p1) => p1.toLowerCase()).replace(/([A-Z])/g, (_, p1) => `_${p1.toLowerCase()}`) as StrategySnakeCase];
-                  const running = problem.running_tasks.some((t: Task) => t.type === 'Solve' && t.content === strategy);
+                  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);
+                    const color = acsWithGraphOptToColor(status, running);
+                    const text = acsWithGraphOptToText(status, running);
 
-                  return <TableCell key={strategy} align="center"><Chip color={color} label={text} /></TableCell>;
-                })
+                    return <TableCell key={strategy} align="center"><Chip color={color} label={text} sx={{ cursor: 'inherit' }} /></TableCell>;
+                  })
               }
                     </TableRow>
                   ))}

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>
     </>
   );

server/src/adf.rs

@@ -515,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()