diff --git a/.editorconfig b/.editorconfig index 0758e62d1..a5fab1256 100644 --- a/.editorconfig +++ b/.editorconfig @@ -28,3 +28,6 @@ max_line_length = unset [**.{yml,yaml,md,tex,cabal}] max_line_length = unset + +[.github/actions/spelling/*] +max_line_length = unset diff --git a/.github/actions/spelling/README.md b/.github/actions/spelling/README.md index 516ec071c..ef73ac266 100644 --- a/.github/actions/spelling/README.md +++ b/.github/actions/spelling/README.md @@ -1,16 +1,17 @@ # check-spelling/check-spelling configuration -| File | Purpose | Format | Info | -| -------------------------------------------------- | -------------------------------------------------------------------------------- | --------------------------------------------------------- | ---------------------------------------------------------------------------------------------------- | -| [dictionary.txt](dictionary.txt) | Replacement dictionary (creating this file will override the default dictionary) | one word per line | [dictionary](https://github.com/check-spelling/check-spelling/wiki/Configuration#dictionary) | -| [allow.txt](allow.txt) | Add words to the dictionary | one word per line (only letters and `'`s allowed) | [allow](https://github.com/check-spelling/check-spelling/wiki/Configuration#allow) | -| [reject.txt](reject.txt) | Remove words from the dictionary (after allow) | grep pattern matching whole dictionary words | [reject](https://github.com/check-spelling/check-spelling/wiki/Configuration-Examples%3A-reject) | -| [excludes.txt](excludes.txt) | Files to ignore entirely | perl regular expression | [excludes](https://github.com/check-spelling/check-spelling/wiki/Configuration-Examples%3A-excludes) | -| [only.txt](only.txt) | Only check matching files (applied after excludes) | perl regular expression | [only](https://github.com/check-spelling/check-spelling/wiki/Configuration-Examples%3A-only) | -| [patterns.txt](patterns.txt) | Patterns to ignore from checked lines | perl regular expression (order matters, first match wins) | [patterns](https://github.com/check-spelling/check-spelling/wiki/Configuration-Examples%3A-patterns) | -| [line_forbidden.patterns](line_forbidden.patterns) | Patterns to flag in checked lines | perl regular expression (order matters, first match wins) | [patterns](https://github.com/check-spelling/check-spelling/wiki/Configuration-Examples%3A-patterns) | -| [expect.txt](expect.txt) | Expected words that aren't in the dictionary | one word per line (sorted, alphabetically) | [expect](https://github.com/check-spelling/check-spelling/wiki/Configuration#expect) | -| [advice.md](advice.md) | Supplement for GitHub comment when unrecognized words are found | GitHub Markdown | [advice](https://github.com/check-spelling/check-spelling/wiki/Configuration-Examples%3A-advice) | +| File | Purpose | Format | Info | +| -------------------------------------------------- | -------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------------- | ---------------------------------------------------------------------------------------------------- | +| [dictionary.txt](dictionary.txt) | Replacement dictionary (creating this file will override the default dictionary) | one word per line | [dictionary](https://github.com/check-spelling/check-spelling/wiki/Configuration#dictionary) | +| [allow.txt](allow.txt) | Add words to the dictionary | one word per line (only letters and `'`s allowed) | [allow](https://github.com/check-spelling/check-spelling/wiki/Configuration#allow) | +| [reject.txt](reject.txt) | Remove words from the dictionary (after allow) | grep pattern matching whole dictionary words | [reject](https://github.com/check-spelling/check-spelling/wiki/Configuration-Examples%3A-reject) | +| [excludes.txt](excludes.txt) | Files to ignore entirely | perl regular expression | [excludes](https://github.com/check-spelling/check-spelling/wiki/Configuration-Examples%3A-excludes) | +| [only.txt](only.txt) | Only check matching files (applied after excludes) | perl regular expression | [only](https://github.com/check-spelling/check-spelling/wiki/Configuration-Examples%3A-only) | +| [patterns.txt](patterns.txt) | Patterns to ignore from checked lines | perl regular expression (order matters, first match wins) | [patterns](https://github.com/check-spelling/check-spelling/wiki/Configuration-Examples%3A-patterns) | +| [candidate.patterns](candidate.patterns) | Patterns that might be worth adding to [patterns.txt](patterns.txt) | perl regular expression with optional comment block introductions (all matches will be suggested) | [candidates](https://github.com/check-spelling/check-spelling/wiki/Feature:-Suggest-patterns) | +| [line_forbidden.patterns](line_forbidden.patterns) | Patterns to flag in checked lines | perl regular expression (order matters, first match wins) | [patterns](https://github.com/check-spelling/check-spelling/wiki/Configuration-Examples%3A-patterns) | +| [expect.txt](expect.txt) | Expected words that aren't in the dictionary | one word per line (sorted, alphabetically) | [expect](https://github.com/check-spelling/check-spelling/wiki/Configuration#expect) | +| [advice.md](advice.md) | Supplement for GitHub comment when unrecognized words are found | GitHub Markdown | [advice](https://github.com/check-spelling/check-spelling/wiki/Configuration-Examples%3A-advice) | Note: you can replace any of these files with a directory by the same name (minus the suffix) and then include multiple files inside that directory (with that suffix) to merge multiple files together. diff --git a/.github/actions/spelling/allow.txt b/.github/actions/spelling/allow.txt index dd76c192e..d04eaf82c 100644 --- a/.github/actions/spelling/allow.txt +++ b/.github/actions/spelling/allow.txt @@ -8,6 +8,7 @@ Bifoldable Bifunctor Bitraversable Circo +DMAX DPoint DSL DVal @@ -22,6 +23,9 @@ HXT Hashable Hovern Hspec +Ints +Komplementstelle +Komplementstellen Leftrightarrow Lexer Linkbeschriftung @@ -36,6 +40,8 @@ Perim Petrinetz Petrinetze Petrinetzes +Petrinetzkandidat +Petrinetzkandidaten Petrinetzknoten Programmierparadigmen QDiagram @@ -83,6 +89,7 @@ forkagain forkend fst fusable +ghc ghci github gpt diff --git a/.github/actions/spelling/candidate.patterns b/.github/actions/spelling/candidate.patterns new file mode 100644 index 000000000..340922d57 --- /dev/null +++ b/.github/actions/spelling/candidate.patterns @@ -0,0 +1,527 @@ +# marker to ignore all code on line +^.*/\* #no-spell-check-line \*/.*$ +# marker to ignore all code on line +^.*\bno-spell-check(?:-line|)(?:\s.*|)$ + +# https://cspell.org/configuration/document-settings/ +# cspell inline +^.*\b[Cc][Ss][Pp][Ee][Ll]{2}:\s*[Dd][Ii][Ss][Aa][Bb][Ll][Ee]-[Ll][Ii][Nn][Ee]\b + +# patch hunk comments +^\@\@ -\d+(?:,\d+|) \+\d+(?:,\d+|) \@\@ .* +# git index header +index (?:[0-9a-z]{7,40},|)[0-9a-z]{7,40}\.\.[0-9a-z]{7,40} + +# cid urls +(['"])cid:.*?\g{-1} + +# data url in parens +\(data:[^)]*?(?:[A-Z]{3,}|[A-Z][a-z]{2,}|[a-z]{3,})[^)]*\) +# data url in quotes +([`'"])data:.*?(?:[A-Z]{3,}|[A-Z][a-z]{2,}|[a-z]{3,}).*\g{-1} +# data url +data:[-a-zA-Z=;:/0-9+]*,\S* + +# https/http/file urls +(?:\b(?:https?|ftp|file)://)[-A-Za-z0-9+&@#/%?=~_|!:,.;]+[-A-Za-z0-9+&@#/%=~_|] + +# mailto urls +mailto:[-a-zA-Z=;:/?%&0-9+@.]{3,} + +# magnet urls +magnet:[?=:\w]+ + +# magnet urls +"magnet:[^"]+" + +# obs: +"obs:[^"]*" + +# The `\b` here means a break, it's the fancy way to handle urls, but it makes things harder to read +# In this examples content, I'm using a number of different ways to match things to show various approaches +# asciinema +\basciinema\.org/a/[0-9a-zA-Z]+ + +# apple +\bdeveloper\.apple\.com/[-\w?=/]+ +# Apple music +\bembed\.music\.apple\.com/fr/playlist/usr-share/[-\w.]+ + +# appveyor api +\bci\.appveyor\.com/api/projects/status/[0-9a-z]+ +# appveyor project +\bci\.appveyor\.com/project/(?:[^/\s"]*/){2}builds?/\d+/job/[0-9a-z]+ + +# Amazon + +# Amazon +\bamazon\.com/[-\w]+/(?:dp/[0-9A-Z]+|) +# AWS S3 +\b\w*\.s3[^.]*\.amazonaws\.com/[-\w/&#%_?:=]* +# AWS execute-api +\b[0-9a-z]{10}\.execute-api\.[-0-9a-z]+\.amazonaws\.com\b +# AWS ELB +\b\w+\.[-0-9a-z]+\.elb\.amazonaws\.com\b +# AWS SNS +\bsns\.[-0-9a-z]+.amazonaws\.com/[-\w/&#%_?:=]* +# AWS VPC +vpc-\w+ + +# While you could try to match `http://` and `https://` by using `s?` in `https?://`, sometimes there +# YouTube url +\b(?:(?:www\.|)youtube\.com|youtu.be)/(?:channel/|embed/|user/|playlist\?list=|watch\?v=|v/|)[-a-zA-Z0-9?&=_%]* +# YouTube music +\bmusic\.youtube\.com/youtubei/v1/browse(?:[?&]\w+=[-a-zA-Z0-9?&=_]*) +# YouTube tag +<\s*youtube\s+id=['"][-a-zA-Z0-9?_]*['"] +# YouTube image +\bimg\.youtube\.com/vi/[-a-zA-Z0-9?&=_]* +# Google Accounts +\baccounts.google.com/[-_/?=.:;+%&0-9a-zA-Z]* +# Google Analytics +\bgoogle-analytics\.com/collect.[-0-9a-zA-Z?%=&_.~]* +# Google APIs +\bgoogleapis\.(?:com|dev)/[a-z]+/(?:v\d+/|)[a-z]+/[-@:./?=\w+|&]+ +# Google Storage +\b[-a-zA-Z0-9.]*\bstorage\d*\.googleapis\.com(?:/\S*|) +# Google Calendar +\bcalendar\.google\.com/calendar(?:/u/\d+|)/embed\?src=[@./?=\w&%]+ +\w+\@group\.calendar\.google\.com\b +# Google DataStudio +\bdatastudio\.google\.com/(?:(?:c/|)u/\d+/|)(?:embed/|)(?:open|reporting|datasources|s)/[-0-9a-zA-Z]+(?:/page/[-0-9a-zA-Z]+|) +# The leading `/` here is as opposed to the `\b` above +# ... a short way to match `https://` or `http://` since most urls have one of those prefixes +# Google Docs +/docs\.google\.com/[a-z]+/(?:ccc\?key=\w+|(?:u/\d+|d/(?:e/|)[0-9a-zA-Z_-]+/)?(?:edit\?[-\w=#.]*|/\?[\w=&]*|)) +# Google Drive +\bdrive\.google\.com/(?:file/d/|open)[-0-9a-zA-Z_?=]* +# Google Groups +\bgroups\.google\.com/(?:(?:forum/#!|d/)(?:msg|topics?|searchin)|a)/[^/\s"]+/[-a-zA-Z0-9$]+(?:/[-a-zA-Z0-9]+)* +# Google Maps +\bmaps\.google\.com/maps\?[\w&;=]* +# Google themes +themes\.googleusercontent\.com/static/fonts/[^/\s"]+/v\d+/[^.]+. +# Google CDN +\bclients2\.google(?:usercontent|)\.com[-0-9a-zA-Z/.]* +# Goo.gl +/goo\.gl/[a-zA-Z0-9]+ +# Google Chrome Store +\bchrome\.google\.com/webstore/detail/[-\w]*(?:/\w*|) +# Google Books +\bgoogle\.(?:\w{2,4})/books(?:/\w+)*\?[-\w\d=&#.]* +# Google Fonts +\bfonts\.(?:googleapis|gstatic)\.com/[-/?=:;+&0-9a-zA-Z]* +# Google Forms +\bforms\.gle/\w+ +# Google Scholar +\bscholar\.google\.com/citations\?user=[A-Za-z0-9_]+ +# Google Colab Research Drive +\bcolab\.research\.google\.com/drive/[-0-9a-zA-Z_?=]* + +# GitHub SHAs (api) +\bapi.github\.com/repos(?:/[^/\s"]+){3}/[0-9a-f]+\b +# GitHub SHAs (markdown) +(?:\[`?[0-9a-f]+`?\]\(https:/|)/(?:www\.|)github\.com(?:/[^/\s"]+){2,}(?:/[^/\s")]+)(?:[0-9a-f]+(?:[-0-9a-zA-Z/#.]*|)\b|) +# GitHub SHAs +\bgithub\.com(?:/[^/\s"]+){2}[@#][0-9a-f]+\b +# GitHub wiki +\bgithub\.com/(?:[^/]+/){2}wiki/(?:(?:[^/]+/|)_history|[^/]+(?:/_compare|)/[0-9a-f.]{40,})\b +# githubusercontent +/[-a-z0-9]+\.githubusercontent\.com/[-a-zA-Z0-9?&=_\/.]* +# githubassets +\bgithubassets.com/[0-9a-f]+(?:[-/\w.]+) +# gist github +\bgist\.github\.com/[^/\s"]+/[0-9a-f]+ +# git.io +\bgit\.io/[0-9a-zA-Z]+ +# GitHub JSON +"node_id": "[-a-zA-Z=;:/0-9+]*" +# Contributor +\[[^\]]+\]\(https://github\.com/[^/\s"]+\) +# GHSA +GHSA(?:-[0-9a-z]{4}){3} + +# GitLab commit +\bgitlab\.[^/\s"]*/\S+/\S+/commit/[0-9a-f]{7,16}#[0-9a-f]{40}\b +# GitLab merge requests +\bgitlab\.[^/\s"]*/\S+/\S+/-/merge_requests/\d+/diffs#[0-9a-f]{40}\b +# GitLab uploads +\bgitlab\.[^/\s"]*/uploads/[-a-zA-Z=;:/0-9+]* +# GitLab commits +\bgitlab\.[^/\s"]*/(?:[^/\s"]+/){2}commits?/[0-9a-f]+\b + +# binanace +accounts.binance.com/[a-z/]*oauth/authorize\?[-0-9a-zA-Z&%]* + +# bitbucket diff +\bapi\.bitbucket\.org/\d+\.\d+/repositories/(?:[^/\s"]+/){2}diff(?:stat|)(?:/[^/\s"]+){2}:[0-9a-f]+ +# bitbucket repositories commits +\bapi\.bitbucket\.org/\d+\.\d+/repositories/(?:[^/\s"]+/){2}commits?/[0-9a-f]+ +# bitbucket commits +\bbitbucket\.org/(?:[^/\s"]+/){2}commits?/[0-9a-f]+ + +# bit.ly +\bbit\.ly/\w+ + +# bitrise +\bapp\.bitrise\.io/app/[0-9a-f]*/[\w.?=&]* + +# bootstrapcdn.com +\bbootstrapcdn\.com/[-./\w]+ + +# cdn.cloudflare.com +\bcdnjs\.cloudflare\.com/[./\w]+ + +# circleci +\bcircleci\.com/gh(?:/[^/\s"]+){1,5}.[a-z]+\?[-0-9a-zA-Z=&]+ + +# gitter +\bgitter\.im(?:/[^/\s"]+){2}\?at=[0-9a-f]+ + +# gravatar +\bgravatar\.com/avatar/[0-9a-f]+ + +# ibm +[a-z.]*ibm\.com/[-_#=:%!?~.\\/\d\w]* + +# imgur +\bimgur\.com/[^.]+ + +# Internet Archive +\barchive\.org/web/\d+/(?:[-\w.?,'/\\+&%$#_:]*) + +# discord +/discord(?:app\.com|\.gg)/(?:invite/)?[a-zA-Z0-9]{7,} + +# Disqus +\bdisqus\.com/[-\w/%.()!?&=_]* + +# medium link +\blink\.medium\.com/[a-zA-Z0-9]+ +# medium +\bmedium\.com/\@?[^/\s"]+/[-\w]+ + +# microsoft +\b(?:https?://|)(?:(?:download\.visualstudio|docs|msdn2?|research)\.microsoft|blogs\.msdn)\.com/[-_a-zA-Z0-9()=./%]* +# powerbi +\bapp\.powerbi\.com/reportEmbed/[^"' ]* +# vs devops +\bvisualstudio.com(?::443|)/[-\w/?=%&.]* +# microsoft store +\bmicrosoft\.com/store/apps/\w+ + +# mvnrepository.com +\bmvnrepository\.com/[-0-9a-z./]+ + +# now.sh +/[0-9a-z-.]+\.now\.sh\b + +# oracle +\bdocs\.oracle\.com/[-0-9a-zA-Z./_?#&=]* + +# chromatic.com +/\S+.chromatic.com\S*[")] + +# codacy +\bapi\.codacy\.com/project/badge/Grade/[0-9a-f]+ + +# compai +\bcompai\.pub/v1/png/[0-9a-f]+ + +# mailgun api +\.api\.mailgun\.net/v3/domains/[0-9a-z]+\.mailgun.org/messages/[0-9a-zA-Z=@]* +# mailgun +\b[0-9a-z]+.mailgun.org + +# /message-id/ +/message-id/[-\w@./%]+ + +# Reddit +\breddit\.com/r/[/\w_]* + +# requestb.in +\brequestb\.in/[0-9a-z]+ + +# sched +\b[a-z0-9]+\.sched\.com\b + +# Slack url +slack://[a-zA-Z0-9?&=]+ +# Slack +\bslack\.com/[-0-9a-zA-Z/_~?&=.]* +# Slack edge +\bslack-edge\.com/[-a-zA-Z0-9?&=%./]+ +# Slack images +\bslack-imgs\.com/[-a-zA-Z0-9?&=%.]+ + +# shields.io +\bshields\.io/[-\w/%?=&.:+;,]* + +# stackexchange -- https://stackexchange.com/feeds/sites +\b(?:askubuntu|serverfault|stack(?:exchange|overflow)|superuser).com/(?:questions/\w+/[-\w]+|a/) + +# Sentry +[0-9a-f]{32}\@o\d+\.ingest\.sentry\.io\b + +# Twitter markdown +\[\@[^[/\]:]*?\]\(https://twitter.com/[^/\s"')]*(?:/status/\d+(?:\?[-_0-9a-zA-Z&=]*|)|)\) +# Twitter hashtag +\btwitter\.com/hashtag/[\w?_=&]* +# Twitter status +\btwitter\.com/[^/\s"')]*(?:/status/\d+(?:\?[-_0-9a-zA-Z&=]*|)|) +# Twitter profile images +\btwimg\.com/profile_images/[_\w./]* +# Twitter media +\btwimg\.com/media/[-_\w./?=]* +# Twitter link shortened +\bt\.co/\w+ + +# facebook +\bfburl\.com/[0-9a-z_]+ +# facebook CDN +\bfbcdn\.net/[\w/.,]* +# facebook watch +\bfb\.watch/[0-9A-Za-z]+ + +# dropbox +\bdropbox\.com/sh?/[^/\s"]+/[-0-9A-Za-z_.%?=&;]+ + +# ipfs protocol +ipfs://[0-9a-z]* +# ipfs url +/ipfs/[0-9a-z]* + +# w3 +\bw3\.org/[-0-9a-zA-Z/#.]+ + +# loom +\bloom\.com/embed/[0-9a-f]+ + +# regex101 +\bregex101\.com/r/[^/\s"]+/\d+ + +# figma +\bfigma\.com/file(?:/[0-9a-zA-Z]+/)+ + +# freecodecamp.org +\bfreecodecamp\.org/[-\w/.]+ + +# image.tmdb.org +\bimage\.tmdb\.org/[/\w.]+ + +# mermaid +\bmermaid\.ink/img/[-\w]+|\bmermaid-js\.github\.io/mermaid-live-editor/#/edit/[-\w]+ + +# Wikipedia +\ben\.wikipedia\.org/wiki/[-\w%.#]+ + +# gitweb +[^"\s]+/gitweb/\S+;h=[0-9a-f]+ + +# HyperKitty lists +/archives/list/[^@/]+\@[^/\s"]*/message/[^/\s"]*/ + +# lists +/thread\.html/[^"\s]+ + +# list-management +\blist-manage\.com/subscribe(?:[?&](?:u|id)=[0-9a-f]+)+ + +# kubectl.kubernetes.io/last-applied-configuration +"kubectl.kubernetes.io/last-applied-configuration": ".*" + +# pgp +\bgnupg\.net/pks/lookup[?&=0-9a-zA-Z]* + +# Spotify +\bopen\.spotify\.com/embed/playlist/\w+ + +# Mastodon +\bmastodon\.[-a-z.]*/(?:media/|\@)[?&=0-9a-zA-Z_]* + +# scastie +\bscastie\.scala-lang\.org/[^/]+/\w+ + +# images.unsplash.com +\bimages\.unsplash\.com/(?:(?:flagged|reserve)/|)[-\w./%?=%&.;]+ + +# pastebin +\bpastebin\.com/[\w/]+ + +# heroku +\b\w+\.heroku\.com/source/archive/\w+ + +# quip +\b\w+\.quip\.com/\w+(?:(?:#|/issues/)\w+)? + +# badgen.net +\bbadgen\.net/badge/[^")\]'\s]+ + +# statuspage.io +\w+\.statuspage\.io\b + +# media.giphy.com +\bmedia\.giphy\.com/media/[^/]+/[\w.?&=]+ + +# tinyurl +\btinyurl\.com/\w+ + +# getopts +\bgetopts\s+(?:"[^"]+"|'[^']+') + +# ANSI color codes +(?:\\(?:u00|x)1b|\x1b)\[\d+(?:;\d+|)m + +# URL escaped characters +\%[0-9A-F][A-F] +# IPv6 +\b(?:[0-9a-fA-F]{0,4}:){3,7}[0-9a-fA-F]{0,4}\b +# c99 hex digits (not the full format, just one I've seen) +0x[0-9a-fA-F](?:\.[0-9a-fA-F]*|)[pP] +# Punycode +\bxn--[-0-9a-z]+ +# sha +sha\d+:[0-9]*[a-f]{3,}[0-9a-f]* +# sha-... -- uses a fancy capture +(['"]|")[0-9a-f]{40,}\g{-1} +# hex runs +\b[0-9a-fA-F]{16,}\b +# hex in url queries +=[0-9a-fA-F]*?(?:[A-F]{3,}|[a-f]{3,})[0-9a-fA-F]*?& +# ssh +(?:ssh-\S+|-nistp256) [-a-zA-Z=;:/0-9+]{12,} + +# PGP +\b(?:[0-9A-F]{4} ){9}[0-9A-F]{4}\b +# GPG keys +\b(?:[0-9A-F]{4} ){5}(?: [0-9A-F]{4}){5}\b +# Well known gpg keys +.well-known/openpgpkey/[\w./]+ + +# uuid: +\b[0-9a-fA-F]{8}-(?:[0-9a-fA-F]{4}-){3}[0-9a-fA-F]{12}\b +# hex digits including css/html color classes: +(?:[\\0][xX]|\\u|[uU]\+|#x?|\%23)[0-9_a-fA-FgGrR]*?[a-fA-FgGrR]{2,}[0-9_a-fA-FgGrR]*(?:[uUlL]{0,3}|u\d+)\b +# integrity +integrity="sha\d+-[-a-zA-Z=;:/0-9+]{40,}" + +# https://www.gnu.org/software/groff/manual/groff.html +# man troff content +\\f[BCIPR] +# ' +\\\(aq + +# .desktop mime types +^MimeTypes?=.*$ +# .desktop localized entries +^[A-Z][a-z]+\[[a-z]+\]=.*$ +# Localized .desktop content +Name\[[^\]]+\]=.* + +# IServiceProvider +\bI(?=(?:[A-Z][a-z]{2,})+\b) + +# crypt +"\$2[ayb]\$.{56}" + +# scrypt / argon +\$(?:scrypt|argon\d+[di]*)\$\S+ + +# Input to GitHub JSON +content: "[-a-zA-Z=;:/0-9+]*=" + +# Python stringprefix / binaryprefix +# Note that there's a high false positive rate, remove the `?=` and search for the regex to see if the matches seem like reasonable strings +(?v# +(?:(?<=[A-Z]{2})V|(?<=[a-z]{2}|[A-Z]{2})v)\d+(?:\b|(?=[a-zA-Z_])) +# Compiler flags (Scala) +(?:^|[\t ,>"'`=(])-J-[DPWXY](?=[A-Z]{2,}|[A-Z][a-z]|[a-z]{2,}) +# Compiler flags +(?:^|[\t ,"'`=(])-[DPWXYLlf](?=[A-Z]{2,}|[A-Z][a-z]|[a-z]{2,}) +# Compiler flags (linker) +,-B +# curl arguments +\b(?:\\n|)curl(?:\s+-[a-zA-Z]{1,2}\b)*(?:\s+-[a-zA-Z]{3,})(?:\s+-[a-zA-Z]+)* +# set arguments +\bset(?:\s+-[abefimouxE]{1,2})*\s+-[abefimouxE]{3,}(?:\s+-[abefimouxE]+)* +# tar arguments +\b(?:\\n|)g?tar(?:\.exe|)(?:(?:\s+--[-a-zA-Z]+|\s+-[a-zA-Z]+|\s[ABGJMOPRSUWZacdfh-pr-xz]+\b)(?:=[^ ]*|))+ +# tput arguments -- https://man7.org/linux/man-pages/man5/terminfo.5.html -- technically they can be more than 5 chars long... +\btput\s+(?:(?:-[SV]|-T\s*\w+)\s+)*\w{3,5}\b +# macOS temp folders +/var/folders/\w\w/[+\w]+/(?:T|-Caches-)/ diff --git a/.github/actions/spelling/line_forbidden.patterns b/.github/actions/spelling/line_forbidden.patterns index 4ca15837c..b755b9c11 100644 --- a/.github/actions/spelling/line_forbidden.patterns +++ b/.github/actions/spelling/line_forbidden.patterns @@ -19,6 +19,12 @@ # s.b. greater than \bgreater then\b +# s.b. into +\sin to\s + +# s.b. opt-in +\sopt in\s + # s.b. less than \bless then\b @@ -30,10 +36,22 @@ \b[Nn]o[nt][- ]existent\b # s.b. preexisting -[Pp]re-existing +[Pp]re[- ]existing + +# s.b. preempt +[Pp]re[- ]empt\b # s.b. preemptively -[Pp]re-emptively +[Pp]re[- ]emptively + +# s.b. reentrancy +[Rr]e[- ]entrancy + +# s.b. reentrant +[Rr]e[- ]entrant + +# s.b. workaround(s) +\bwork[- ]arounds?\b # Reject duplicate words \s([A-Z]{3,}|[A-Z][a-z]{2,}|[a-z]{3,})\s\g{-1}\s diff --git a/.github/actions/spelling/patterns.txt b/.github/actions/spelling/patterns.txt index 3820c077b..086cb8f5b 100644 --- a/.github/actions/spelling/patterns.txt +++ b/.github/actions/spelling/patterns.txt @@ -1,6 +1,5 @@ # See https://github.com/check-spelling/check-spelling/wiki/Configuration-Examples:-patterns -# acceptable duplicates # ls directory listings [-bcdlpsw](?:[-r][-w][-sx]){3}\s+\d+\s+(\S+)\s+\g{-1}\s+\d+\s+ # C types @@ -8,14 +7,20 @@ # javadoc / .net (?:\@(?:groupname|param)|(?:public|private)(?:\s+static|\s+readonly)*)\s+(\w+)\s+\g{-1}\s +# Commit message -- Signed-off-by and friends +^\s*(?:(?:Based-on-patch|Co-authored|Helped|Mentored|Reported|Reviewed|Signed-off)-by|Thanks-to): (?:[^<]*<[^>]*>|[^<]*)\s*$ + +# Autogenerated revert commit message +^This reverts commit [0-9a-f]{40}\.$ + # ignore long runs of a single character: \b([A-Za-z])\g{-1}{3,}\b # ignore urls https?://[-+0-9a-zA-Z?&=_\/%.]* -# ignore GHC compiler instructions -^\{-# OPTIONS_GHC .* #-}$ +# GHC LANGUAGE extension, HLINT options etc. +^\{-# .* #-}$ # ignore renaming advices ^Original: [a-zA-Z0-9]+ ––– Here: [a-zA-Z0-9]+$ @@ -34,6 +39,7 @@ Nothing\sNothing String\sString True\sTrue False\sFalse + getDoubleAs\slabel\signore\signore obj\sobj\ssig diff --git a/.github/actions/spelling/reject.txt b/.github/actions/spelling/reject.txt index b5a6d3680..a025b3dd9 100644 --- a/.github/actions/spelling/reject.txt +++ b/.github/actions/spelling/reject.txt @@ -1,5 +1,6 @@ ^attache$ benefitting +formulae occurences? ^dependan.* ^oer$ diff --git a/.github/workflows/hlint.yml b/.github/workflows/hlint.yml index 2a1fdb9fc..4da588914 100644 --- a/.github/workflows/hlint.yml +++ b/.github/workflows/hlint.yml @@ -27,7 +27,7 @@ jobs: - name: "Set up HLint" uses: haskell-actions/hlint-setup@v2 with: - version: "3.5" + version: latest - name: "Run HLint" uses: haskell-actions/hlint-run@v2 diff --git a/README.md b/README.md index 0e150002c..be6e6b6ac 100644 --- a/README.md +++ b/README.md @@ -9,6 +9,19 @@ The diagram types covered are - Object diagram (UML) - Petri net +## Configuration + +You may limit the maximal bit width by adding a limit (here 5) to your +`stack.yaml` or `stack-*.yaml` like: + +```haskell +ghc-options: + autotool-capabilities: -DMAX_BIT_WIDTH=5 +``` + +This configuration is then used in order to reject configurations that do not +adhere to this limit. + ## Compatibility On Windows, you may have to use `SAT4J` instead of `MiniSat`. diff --git a/alloy/petri/PetriConcepts.als b/alloy/petri/PetriConcepts.als index 430960987..580701c4c 100644 --- a/alloy/petri/PetriConcepts.als +++ b/alloy/petri/PetriConcepts.als @@ -39,7 +39,7 @@ pred concurrentDefault[ts : set givenTransitions]{ all p : givenPlaces | p.defaultTokens >= (sum t : ts | p.defaultFlow[t]) } -//check if there is a loop between two nodes +//check if there is a loop between two nodes (in legal Petri nets; otherwise has slightly different meaning) pred selfLoop[n : Nodes]{ n in n.flow.Int.flow.Int } @@ -53,3 +53,13 @@ pred sinkTransitions[ts : set Transitions]{ pred sourceTransitions[ts : set Transitions]{ no Nodes.flow[ts] // under assumption of valid Petri nets, could use Places instead of Nodes here } + +//check if some transitions are sink transitions under default condition +pred sinkTransitionsDefault[ts : set givenTransitions]{ + no ts.defaultFlow +} + +//check if some transitions are source transitions under default condition +pred sourceTransitionsDefault[ts : set givenTransitions]{ + no givenPlaces.defaultFlow[ts] +} diff --git a/alloy/petri/PetriSignature.als b/alloy/petri/PetriSignature.als index 4277bb5f3..dc64daeb5 100644 --- a/alloy/petri/PetriSignature.als +++ b/alloy/petri/PetriSignature.als @@ -31,7 +31,7 @@ abstract sig Transitions extends Nodes defaultFlow.Int in Places } -fact isLegalPetriNet { +pred isLegalPetriNet { all w : Nodes.flow[Nodes] | w > 0 Places.flow.Int in Transitions Transitions.flow.Int in Places diff --git a/app/capacity.hs b/app/capacity.hs new file mode 100644 index 000000000..e27d8ce1e --- /dev/null +++ b/app/capacity.hs @@ -0,0 +1,106 @@ +{-# Language DuplicateRecordFields #-} +{-# Language RecordWildCards #-} + +module Main (main) where + +import Capabilities.Alloy.IO () +import Capabilities.Cache.IO () +import Capabilities.Diagrams.IO () +import Capabilities.Graphviz.IO () +import Common ( + forceErrors, + instanceInput, + withLang, + ) +import Modelling.PetriNet.Capacity ( + checkCapacityConfigs, + capacityGenerate, + simpleCapacityTask, + ) +import Modelling.PetriNet.Types ( + BasicConfig(..), + CapacityConfig(..), + defaultCapacityConfig, + ) + +import Control.OutputCapable.Blocks (Language (English)) +import Control.Monad.Trans.Class (lift) +import Data.Maybe (isNothing) +import System.IO ( + BufferMode (NoBuffering), hSetBuffering, stdout, + ) +import Text.Pretty.Simple (pPrint) +import Text.Read (readMaybe) + +main :: IO () +main = do + hSetBuffering stdout NoBuffering + putStrLn "Generating instance for converting nets with capacities into nets without capacities" + i <- instanceInput + if i >= 0 + then mainFind i + else print "There is no negative index" + +mainFind :: Int -> IO () +mainFind i = forceErrors $ do + let theConfig@CapacityConfig{..} = defaultCapacityConfig + lift $ pPrint theConfig + (pls, trns, maxCap, newFlowMin, newFlowMax, oneMin, distractMin, distractMax, atMostAct) <- lift $ userInput theConfig + let config = theConfig { + basicConfig = basicConfig { + places = pls, + transitions = trns + }, + maxCapacity = maxCap, + newArrowsWithComplement = (newFlowMin, newFlowMax), + oneMinCapacity = oneMin, + distractors = (distractMin, distractMax), + atMostActive = atMostAct + } :: CapacityConfig + let c = checkCapacityConfigs config + if isNothing c + then do + t <- capacityGenerate config 0 i + lift . (`withLang` English) $ simpleCapacityTask "tmp/" t + lift $ print t + else + lift $ print c + +validateInput :: Read a => a -> IO a +validateInput d = do + input <- getLine + if null input then return d + else case readMaybe input of + Just n -> return n + Nothing -> do + putStrLn "Invalid input" + validateInput d + +userInput :: CapacityConfig -> IO (Int, Int, Int, Int, Int, Int, Int, Int, Maybe Int) +userInput CapacityConfig{ + basicConfig = BasicConfig{..}, + maxCapacity = maxCapacity, + newArrowsWithComplement = (minNewFlowMin, minNewFlowMax), + oneMinCapacity = oneMinCapacity, + distractors = (distractorsMin, distractorsMax), + atMostActive = atMost + } = do + putStr "Number of Places: " + pls <- validateInput places + putStr "Number of Transitions: " + trns <- validateInput transitions + putStr "Highest capacity for a place: " + maxCap <- validateInput maxCapacity + putStr "How many new arrows are at minimum connected to complement places: " + newFlowMin <- validateInput minNewFlowMin + putStr "How many new arrows are at maximum connected to complement places: " + newFlowMax <- validateInput minNewFlowMax + putStr "What capacity should one place at least have: " + oneMin <- validateInput oneMinCapacity + putStr "How many distractors (transitions that are activated, but not given the capacity) at minimum: " + distractMin <- validateInput distractorsMin + putStr "How many distractors (transitions that are activated, but not given the capacity) at maximum: " + distractMax <- validateInput distractorsMax + putStr "Maximum number of active Transitions (Just Int/Nothing): " + atMostAct <- validateInput atMost + return (pls, trns, maxCap, newFlowMin, newFlowMax, oneMin, distractMin, distractMax, atMostAct) diff --git a/app/findActivatedTransitions.hs b/app/findActivatedTransitions.hs new file mode 100644 index 000000000..7981b4e1d --- /dev/null +++ b/app/findActivatedTransitions.hs @@ -0,0 +1,92 @@ +{-# Language DuplicateRecordFields #-} +{-# Language RecordWildCards #-} + +module Main (main) where + +import Capabilities.Alloy.IO () +import Capabilities.Cache.IO () +import Capabilities.Diagrams.IO () +import Capabilities.Graphviz.IO () +import Common ( + forceErrors, + instanceInput, + withLang, + ) +import Modelling.PetriNet.FindActivatedTransitions ( + checkFindActivatedTransitionsConfig, + findActivatedTransitionsGenerate, + simpleFindActivatedTransitionsTask, + ) +import Modelling.PetriNet.Types ( + BasicConfig(..), + ChangeConfig(..), + FindActivatedTransitionsConfig(..), + defaultFindActivatedTransitionsConfig, + ) + +import Control.OutputCapable.Blocks (Language (English)) +import Control.Monad.Trans.Class (lift) +import Data.Maybe (isNothing) +import System.IO ( + BufferMode (NoBuffering), hSetBuffering, stdout, + ) +import Text.Pretty.Simple (pPrint) +import Text.Read (readMaybe) + +main :: IO () +main = do + hSetBuffering stdout NoBuffering + putStrLn "Generating instance for finding activated transition(s) in a net" + i <- instanceInput + if i >= 0 + then mainFind i + else print "There is no negative index" + +mainFind :: Int -> IO () +mainFind i = forceErrors $ do + let theConfig@FindActivatedTransitionsConfig{..} = defaultFindActivatedTransitionsConfig + lift $ pPrint theConfig + (pls, trns, tknChange, flwChange, atMost) <- lift $ userInput theConfig + let config = theConfig { + basicConfig = basicConfig { + places = pls, + transitions = trns + }, + changeConfig = changeConfig { + tokenChangeOverall = tknChange, + flowChangeOverall = flwChange + }, + atMostActive = atMost + } :: FindActivatedTransitionsConfig + let c = checkFindActivatedTransitionsConfig config + if isNothing c + then do + t <- findActivatedTransitionsGenerate config 0 i + lift . (`withLang` English) $ simpleFindActivatedTransitionsTask "tmp/" t + lift $ print t + else + lift $ print c + +validateInput :: Read a => a -> IO a +validateInput d = do + input <- getLine + if null input then return d + else case readMaybe input of + Just n -> return n + Nothing -> do + putStrLn "Invalid input" + validateInput d + +userInput :: FindActivatedTransitionsConfig -> IO (Int, Int, Int, Int, Maybe Int) +userInput FindActivatedTransitionsConfig{basicConfig = BasicConfig{..}, changeConfig = ChangeConfig{..}, atMostActive = atMostActiveValue} = do + putStr "Number of Places: " + pls <- validateInput places + putStr "Number of Transitions: " + trns <- validateInput transitions + putStr "TokenChange Overall: " + tknCh <- validateInput tokenChangeOverall + putStr "FlowChange Overall: " + flwCh <- validateInput flowChangeOverall + putStr "AtMostActive Transitions (Just Int/Nothing): " + atMost <- validateInput atMostActiveValue + return (pls, trns, tknCh, flwCh, atMost) diff --git a/app/modelling-tasks-apps.cabal b/app/modelling-tasks-apps.cabal index 0f4160982..88b1556a7 100644 --- a/app/modelling-tasks-apps.cabal +++ b/app/modelling-tasks-apps.cabal @@ -8,6 +8,33 @@ name: modelling-tasks-apps version: 0.0.0 build-type: Simple +executable capacity + main-is: capacity.hs + other-modules: + Common + hs-source-dirs: + ./ + common + ghc-options: -Wall -Wincomplete-uni-patterns -Wincomplete-record-updates -Widentities -Wredundant-constraints -Werror -Wwarn=incomplete-uni-patterns -Wwarn=orphans -Wwarn=unrecognised-warning-flags -Wwarn=x-partial + build-tools: + alex + , happy + build-depends: + MonadRandom + , autotool-capabilities-io-instances + , base + , bytestring + , containers + , diagrams-lib + , diagrams-svg + , digest + , modelling-tasks + , mtl + , output-blocks + , pretty-simple + , transformers + default-language: Haskell2010 + executable check-cds main-is: check-cds.hs hs-source-dirs: @@ -189,6 +216,33 @@ executable evalTimeToGenerate , transformers default-language: Haskell2010 +executable findActivatedTransitions + main-is: findActivatedTransitions.hs + other-modules: + Common + hs-source-dirs: + ./ + common + ghc-options: -Wall -Wincomplete-uni-patterns -Wincomplete-record-updates -Widentities -Wredundant-constraints -Werror -Wwarn=incomplete-uni-patterns -Wwarn=orphans -Wwarn=unrecognised-warning-flags -Wwarn=x-partial + build-tools: + alex + , happy + build-depends: + MonadRandom + , autotool-capabilities-io-instances + , base + , bytestring + , containers + , diagrams-lib + , diagrams-svg + , digest + , modelling-tasks + , mtl + , output-blocks + , pretty-simple + , transformers + default-language: Haskell2010 + executable findAuxiliaryPetriNodesTaskDemo main-is: findAuxiliaryPetriNodesTaskDemo.hs other-modules: @@ -315,6 +369,33 @@ executable matchToMath , transformers default-language: Haskell2010 +executable pickMistake + main-is: pickMistake.hs + other-modules: + Common + hs-source-dirs: + ./ + common + ghc-options: -Wall -Wincomplete-uni-patterns -Wincomplete-record-updates -Widentities -Wredundant-constraints -Werror -Wwarn=incomplete-uni-patterns -Wwarn=orphans -Wwarn=unrecognised-warning-flags -Wwarn=x-partial + build-tools: + alex + , happy + build-depends: + MonadRandom + , autotool-capabilities-io-instances + , base + , bytestring + , containers + , diagrams-lib + , diagrams-svg + , digest + , modelling-tasks + , mtl + , output-blocks + , pretty-simple + , transformers + default-language: Haskell2010 + executable repair-incorrect main-is: repair-incorrect.hs other-modules: diff --git a/app/package.yaml b/app/package.yaml index 2c1a24cb1..63c30c1ce 100644 --- a/app/package.yaml +++ b/app/package.yaml @@ -23,6 +23,20 @@ dependencies: - mtl - transformers executables: + capacity: + main: capacity.hs + source-dirs: + - . + - common + dependencies: + - autotool-capabilities-io-instances + - bytestring + - digest + - modelling-tasks + - output-blocks + - pretty-simple + other-modules: + - Common check-cds: main: check-cds.hs source-dirs: . @@ -107,6 +121,20 @@ executables: - criterion-measurement - modelling-tasks - string-interpolate + findActivatedTransitions: + main: findActivatedTransitions.hs + source-dirs: + - . + - common + dependencies: + - autotool-capabilities-io-instances + - bytestring + - digest + - modelling-tasks + - output-blocks + - pretty-simple + other-modules: + - Common findAuxiliaryPetriNodesTaskDemo: main: findAuxiliaryPetriNodesTaskDemo.hs source-dirs: @@ -168,6 +196,20 @@ executables: - pretty-simple other-modules: - Common + pickMistake: + main: pickMistake.hs + source-dirs: + - . + - common + dependencies: + - autotool-capabilities-io-instances + - bytestring + - digest + - modelling-tasks + - output-blocks + - pretty-simple + other-modules: + - Common repair-incorrect: main: repair-incorrect.hs source-dirs: diff --git a/app/pickMistake.hs b/app/pickMistake.hs new file mode 100644 index 000000000..6f929a857 --- /dev/null +++ b/app/pickMistake.hs @@ -0,0 +1,101 @@ +{-# Language DuplicateRecordFields #-} +{-# Language RecordWildCards #-} + +module Main (main) where + +import Capabilities.Alloy.IO () +import Capabilities.Cache.IO () +import Capabilities.Diagrams.IO () +import Capabilities.Graphviz.IO () +import Common ( + forceErrors, + instanceInput, + withLang, + ) +import Modelling.PetriNet.PickMistake ( + checkPickMistakeConfig, + pickMistakeGenerate, + simplePickMistakeTask, + ) +import Modelling.PetriNet.Types ( + BasicConfig (..), + ChangeConfig (..), + MistakeConfig (..), + PickMistakeConfig (..), + defaultPickMistakeConfig, + ) + +import Control.OutputCapable.Blocks (Language (English)) +import Control.Monad.Trans.Class (lift) +import Data.Maybe (isNothing) +import System.IO ( + BufferMode (NoBuffering), hSetBuffering, stdout, + ) +import Text.Pretty.Simple (pPrint) +import Text.Read (readMaybe) + +main :: IO () +main = do + hSetBuffering stdout NoBuffering + putStrLn "Generating instance for picking the Net with mistakes" + i <- instanceInput + if i >= 0 + then mainPick i + else print "There is no negative index" + +mainPick :: Int -> IO () +mainPick i = forceErrors $ do + let theConfig@PickMistakeConfig{..} = defaultPickMistakeConfig + lift $ pPrint theConfig + (pls, trns, tknChange, flwChange, negWeight, transToTr, placeToPl) <- lift $ userInput theConfig + let config = theConfig { + basicConfig = basicConfig { + places = pls, + transitions = trns + }, + changeConfig = changeConfig { + tokenChangeOverall = tknChange, + flowChangeOverall = flwChange + }, + mistakeConfig = mistakeConfig { + canHaveNegativeWeight = negWeight, + canHaveTransitionToTransition = transToTr, + canHavePlaceToPlace = placeToPl + } + } :: PickMistakeConfig + let c = checkPickMistakeConfig config + if isNothing c + then do + t <- pickMistakeGenerate config 0 i + lift . (`withLang` English) $ simplePickMistakeTask "tmp/" t + lift $ print t + else + lift $ print c + +validateInput :: Read a => a -> IO a +validateInput d = do + input <- getLine + if null input then return d + else case readMaybe input of + Just n -> return n + Nothing -> do + putStrLn "Invalid input" + validateInput d + +userInput :: PickMistakeConfig -> IO (Int, Int, Int, Int, Bool, Bool, Bool) +userInput PickMistakeConfig{basicConfig = BasicConfig{..}, changeConfig = ChangeConfig{..}, mistakeConfig = MistakeConfig{..}} = do + putStr "Number of Places: " + pls <- validateInput places + putStr "Number of Transitions: " + trns <- validateInput transitions + putStr "TokenChange Overall: " + tknCh <- validateInput tokenChangeOverall + putStr "FlowChange Overall: " + flwCh <- validateInput flowChangeOverall + putStr "Negative Token Cost (True/False): " + negWeight <- validateInput canHaveNegativeWeight + putStr "Transition to Transition (True/False): " + transToTr <- validateInput canHaveTransitionToTransition + putStr "Places to Places (True/False): " + placeToPl <- validateInput canHavePlaceToPlace + return (pls, trns, tknCh, flwCh, negWeight, transToTr, placeToPl) diff --git a/modelling-tasks.cabal b/modelling-tasks.cabal index 7ff7144a5..4a690ac46 100644 --- a/modelling-tasks.cabal +++ b/modelling-tasks.cabal @@ -70,11 +70,14 @@ library Modelling.PetriNet.MatchToMath Modelling.PetriNet.Parser Modelling.PetriNet.Types + Modelling.PetriNet.Capacity Modelling.PetriNet.Concurrency Modelling.PetriNet.Conflict Modelling.PetriNet.ConflictPlaces Modelling.PetriNet.Find + Modelling.PetriNet.FindActivatedTransitions Modelling.PetriNet.Pick + Modelling.PetriNet.PickMistake Modelling.PetriNet.Reach.Deadlock Modelling.PetriNet.Reach.Draw Modelling.PetriNet.Reach.Filter @@ -84,6 +87,7 @@ library Modelling.PetriNet.Reach.Type Modelling.Types other-modules: + Configuration Modelling.ActivityDiagram.Auxiliary.ActionSequences Modelling.ActivityDiagram.Auxiliary.PetriValidation Modelling.Auxiliary.Diagrams @@ -173,10 +177,13 @@ test-suite modelling-tasks-test Modelling.CdOd.SelectValidCdSpec Modelling.Common Modelling.PetriNet.AlloySpec + Modelling.PetriNet.CapacitySpec Modelling.PetriNet.ConcurrencySpec Modelling.PetriNet.ConflictSpec Modelling.PetriNet.DiagramSpec + Modelling.PetriNet.FindActivatedTransitionsSpec Modelling.PetriNet.MatchToMathSpec + Modelling.PetriNet.PickMistakeSpec Modelling.PetriNet.Reach.DeadlockSpec Modelling.PetriNet.Reach.FilterSpec Modelling.PetriNet.Reach.ReachSpec diff --git a/package.yaml b/package.yaml index a8d200e7d..b09b67fc6 100644 --- a/package.yaml +++ b/package.yaml @@ -118,11 +118,14 @@ library: - Modelling.PetriNet.MatchToMath - Modelling.PetriNet.Parser - Modelling.PetriNet.Types + - Modelling.PetriNet.Capacity - Modelling.PetriNet.Concurrency - Modelling.PetriNet.Conflict - Modelling.PetriNet.ConflictPlaces - Modelling.PetriNet.Find + - Modelling.PetriNet.FindActivatedTransitions - Modelling.PetriNet.Pick + - Modelling.PetriNet.PickMistake - Modelling.PetriNet.Reach.Deadlock - Modelling.PetriNet.Reach.Draw - Modelling.PetriNet.Reach.Filter diff --git a/src/Configuration.hs b/src/Configuration.hs new file mode 100644 index 000000000..aa0fe49a0 --- /dev/null +++ b/src/Configuration.hs @@ -0,0 +1,3 @@ +-- | + +module Configuration where diff --git a/src/Modelling/CdOd/Types.hs b/src/Modelling/CdOd/Types.hs index 2d45086be..ac52e7fdf 100644 --- a/src/Modelling/CdOd/Types.hs +++ b/src/Modelling/CdOd/Types.hs @@ -738,10 +738,10 @@ checkClassConfigWithProperties | Just False == y = 0 | otherwise = x plusOne x = if x /= 0 then x + 1 else x - minNonInheritances = (+ selfRelationshipsAmount) . plusOne $ sum [ - 1 `forMaybe` hasDoubleRelationships, - 1 `forMaybe` hasReverseRelationships - ] + minNonInheritances = (+ selfRelationshipsAmount) . plusOne $ ( + (1 `forMaybe` hasDoubleRelationships) + + (1 `forMaybe` hasReverseRelationships) + ) minInheritances = (+ selfInheritancesAmount) . plusOne $ sum [ 1 `for` hasReverseInheritances, 1 `forMaybe` hasMultipleInheritances, diff --git a/src/Modelling/PetriNet/Alloy.hs b/src/Modelling/PetriNet/Alloy.hs index 7614ee88b..78484f23e 100644 --- a/src/Modelling/PetriNet/Alloy.hs +++ b/src/Modelling/PetriNet/Alloy.hs @@ -12,14 +12,14 @@ module Modelling.PetriNet.Alloy ( compChange, connected, defaultConstraints, + enforceConstraints, isolated, moduleHelpers, modulePetriAdditions, modulePetriConcepts, modulePetriConstraints, modulePetriSignature, - petriScopeBitWidth, - petriScopeMaxSeq, + randomInSegment, signatures, skolemVariable, taskInstance, @@ -55,6 +55,7 @@ import Control.Monad.Random ( import Data.Composition ((.:)) import Data.FileEmbed (embedStringFile) import Data.List (intercalate) +import Data.Maybe (isJust) import Data.Set (Set) import Data.String.Interpolate (i) import Language.Alloy.Call ( @@ -64,17 +65,6 @@ import Language.Alloy.Call ( unscoped, ) -petriScopeBitWidth :: BasicConfig -> Int -petriScopeBitWidth BasicConfig - { flowOverall, places, tokensOverall, transitions } = - floor - (2 + ((logBase :: Double -> Double -> Double) 2.0 . fromIntegral) - (maximum [snd flowOverall, snd tokensOverall, places, transitions]) - ) - -petriScopeMaxSeq :: BasicConfig -> Int -petriScopeMaxSeq BasicConfig{places,transitions} = places+transitions - modulePetriSignature :: String modulePetriSignature = removeLines 2 $(embedStringFile "alloy/petri/PetriSignature.als") @@ -98,12 +88,18 @@ A set of constraints enforcing settings of 'BasicConfig'. (Besides 'defaultConstraints') -} compBasicConstraints - :: String + :: Bool + -- ^ 'True' for legal petri nets, `False` for illegal petri nets. + -> Maybe Int + -- ^ Whether or not to enforce a maximum number of activated transitions. + -> String -- ^ The name of the Alloy variable for the set of activated Transitions. -> BasicConfig -- ^ the configuration to enforce. -> String -compBasicConstraints = enforceConstraints False +compBasicConstraints legal atMostActive activated basicConfig = [i| + #{enforceConstraints False atMostActive activated basicConfig} + #{if legal then "isLegalPetriNet" else "not isLegalPetriNet"}|] {-| A set of constraints enforcing settings of 'BasicConfig' for the net under @@ -115,17 +111,19 @@ defaultConstraints -> BasicConfig -- ^ the configuration to enforce. -> String -defaultConstraints = enforceConstraints True +defaultConstraints = enforceConstraints True Nothing enforceConstraints :: Bool -- ^ If to generate constraints under default conditions. + -> Maybe Int + -- ^ Whether or not to enforce a maximum number of activated transitions. -> String -- ^ The name of the Alloy variable for the set of activated Transitions. -> BasicConfig -- ^ the configuration to enforce. -> String -enforceConstraints underDefault activated BasicConfig { +enforceConstraints underDefault atMostActive activated BasicConfig { atLeastActive, isConnected, flowOverall, @@ -139,8 +137,7 @@ enforceConstraints underDefault activated BasicConfig { all w : #{nodes}.#{flow}[#{nodes}] | w =< #{maxFlowPerEdge} let theFlow = (sum f, t : #{nodes} | f.#{flow}[t]) | #{fst flowOverall} =< theFlow and theFlow =< #{snd flowOverall} - \##{activated} >= #{atLeastActive} - theActivated#{upperFirst which}Transitions[#{activated}] + #{activatedConstraint} #{connected (prepend "graphIsConnected") isConnected} #{isolated (prepend "noIsolatedNodes") isConnected}|] where @@ -151,6 +148,14 @@ enforceConstraints underDefault activated BasicConfig { nodes = given "Nodes" places = given "Places" tokens = prepend "tokens" + activatedConstraint = unlines $ + [ '#' : activated ++ " >= " ++ show atLeastActive | atLeastActive > 0 ] + ++ + [ " theActivated" ++ upperFirst which ++ "Transitions[" ++ activated ++ "]" | atLeastActive > 0 || isJust atMostActive ] + ++ case atMostActive of + Just 0 -> [ " no " ++ activated ] + Just atMost -> [ " #" ++ activated ++ " =< " ++ show atMost ] + Nothing -> [] connected :: String -> Maybe Bool -> String connected p = maybe "" $ \c -> (if c then "" else "not ") ++ p @@ -158,8 +163,8 @@ connected p = maybe "" $ \c -> (if c then "" else "not ") ++ p isolated :: String -> Maybe Bool -> String isolated p = maybe p $ \c -> if c then "" else p -compAdvConstraints :: AdvConfig -> String -compAdvConstraints AdvConfig +compAdvConstraints :: Bool -> AdvConfig -> String +compAdvConstraints underDefault AdvConfig { presenceOfSelfLoops, presenceOfSinkTransitions , presenceOfSourceTransitions } = [i| @@ -172,11 +177,13 @@ compAdvConstraints AdvConfig True -> "some n : Nodes | selfLoop[n]" False -> "no n : Nodes | selfLoop[n]" petriSink = \case - True -> "some t : Transitions | sinkTransitions[t]" - False -> "no t : Transitions | sinkTransitions[t]" + True -> "some t : " ++ addGiven ++ "Transitions | sinkTransitions" ++ addDefault ++ "[t]" + False -> "no t : " ++ addGiven ++ "Transitions | sinkTransitions" ++ addDefault ++ "[t]" petriSource = \case - True -> "some t : Transitions | sourceTransitions[t]" - False -> "no t : Transitions | sourceTransitions[t]" + True -> "some t : " ++ addGiven ++ "Transitions | sourceTransitions" ++ addDefault ++ "[t]" + False -> "no t : " ++ addGiven ++ "Transitions | sourceTransitions" ++ addDefault ++ "[t]" + addDefault = if underDefault then "Default" else "" + addGiven = if underDefault then "given" else "" compChange :: ChangeConfig -> String compChange ChangeConfig @@ -243,11 +250,11 @@ randomInSegment segment segLength = do unscopedSingleSig :: MonadThrow m - => AlloyInstance - -> String + => String -> String + -> AlloyInstance -> m (Set Object) -unscopedSingleSig inst st nd = do +unscopedSingleSig st nd inst = do sig <- lookupSig (unscoped st) inst getSingleAs nd (return .: Object) sig diff --git a/src/Modelling/PetriNet/Capacity.hs b/src/Modelling/PetriNet/Capacity.hs new file mode 100644 index 000000000..15f50516e --- /dev/null +++ b/src/Modelling/PetriNet/Capacity.hs @@ -0,0 +1,682 @@ +{-# LANGUAGE ApplicativeDo #-} +{-# LANGUAGE DuplicateRecordFields #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE TupleSections #-} + +module Modelling.PetriNet.Capacity ( + CapacityInstance (..), + capacityEvaluation, + capacityGenerate, + capacitySyntax, + capacityTask, + checkCapacityConfig, + checkCapacityConfigs, + combinedCapacity, + combinedCapacityInstance, + defaultCapacityInstance, + findCapacityInstance, + petriNetFindCapacity, + parseCapacityPrec, + simpleCapacityTask, + ) where + +import qualified Modelling.PetriNet.Reach.Type as Reach ( + Place(..), + Transition(..), + ) +import qualified Modelling.PetriNet.Types as Find ( + AlloyConfig (maxInstances, timeout), + CapacityConfig (..), + ) +import qualified Modelling.PetriNet.Types as Pick ( + CapacityConfig (..), + ) +import qualified Data.Bimap as BM ( + lookup, + ) +import qualified Data.Set as Set +import qualified Data.Map as M ( + empty, + fromList, + ) + +import Capabilities.Alloy (MonadAlloy, getInstances) +import Capabilities.Cache (MonadCache) +import Capabilities.Diagrams (MonadDiagrams) +import Capabilities.Graphviz (MonadGraphviz) +import Modelling.Auxiliary.Common ( + TaskGenerationException (NoInstanceAvailable), + oneOf, + ) +import Modelling.Auxiliary.Output ( + hoveringInformation, + ) +import Modelling.PetriNet.Alloy ( + compAdvConstraints, + enforceConstraints, + moduleHelpers, + modulePetriAdditions, + modulePetriConcepts, + modulePetriConstraints, + modulePetriSignature, + randomInSegment, + ) +import Modelling.PetriNet.Diagram ( + cacheNet, + cacheNetWithCapacity, + ) +import Modelling.PetriNet.Find ( + prohibitHidePlaceNames, + prohibitHideTransitionNames, + prohibitPatchworkRenderer, + toFindEvaluationTupleList, + ) +import Modelling.PetriNet.FindActivatedTransitions ( + checkActivatedTransitionsConfig, + ) +import Modelling.PetriNet.Parser ( + addCapacities, + parseChange, + parseNet, + parseRenamedNet, + doubleSig, + singleSig, + ) +import Modelling.PetriNet.Reach.Type ( + parsePlacePrec, + parseTransitionPrec, + ) +import Modelling.PetriNet.Types ( + AdvConfig (..), + AlloyConfig (..), + BasicConfig (..), + Capacity (..), + CapacityConfig (..), + DrawSettings (..), + GraphConfig (..), + Net (traverseNet), + PetriChangeList (..), + PetriLike (PetriLike, allNodes), + SimpleNode (..), + CapacityNode (..), + basicConfigBitWidthInput, + checkBasicConfig, + petriScopeBitWidth, + toChangeList, + ) + +import Control.Applicative ((<|>)) +import Control.Monad (void, when, (>=>)) +import Control.Monad.Catch (MonadThrow, MonadThrow (throwM)) +import Control.OutputCapable.Blocks ( + ArticleToUse (DefiniteArticle), + GenericOutputCapable (..), + LangM', + LangM, + OutputCapable, + Rated, + ($=<<), + continueOrAbort, + english, + german, + printSolutionAndAssert, + translate, + translations, + unLangM + ) +import Control.Monad.Random ( + RandT, + RandomGen, + evalRandT, + mkStdGen + ) +import Control.Monad.Trans (MonadTrans (lift)) +import Data.Bifunctor (first) +import Data.Bitraversable (bimapM) +import Data.Foldable (for_) +import Data.GraphViz.Commands (GraphvizCommand (Circo)) +import Data.List (intercalate) +import Data.Maybe (fromMaybe) +import Data.String.Interpolate (i, iii) +import Text.Parsec ( + char, + optionMaybe, + sepBy, + spaces, + ) +import Text.Parsec.Char (digit) +import Text.Parsec.Combinator (many1) +import Text.Parsec.String (Parser) +import Text.Read (readMaybe) +import Language.Alloy.Call (AlloyInstance) + + +data CapacityInstance = CapacityInstance { + drawWith :: !DrawSettings, + toFind :: !(PetriChangeList String), + originalNet :: !(PetriLike CapacityNode String), + transformedNet :: !(PetriLike SimpleNode String), + complementMap :: ![(String, String)], + numberOfPlaces :: !Int, + numberOfTransitions :: !Int, + showSolution :: !Bool + } + deriving (Show) + +capacityGenerate + :: (MonadAlloy m, MonadThrow m) + => CapacityConfig + -> Int + -> Int + -> m CapacityInstance +capacityGenerate config seed segment = + flip evalRandT (mkStdGen seed) $ do + gl <- oneOf $ graphLayouts gc + + (original, transformed, condition, complementMap) <- combinedCapacityInstance config segment + + let addMissingToCondition changes@ChangeList{tokenChanges} = + let missing = [ (p, 0) + | p <- map snd complementMap + , p `notElem` map fst tokenChanges + ] + in changes { tokenChanges = tokenChanges ++ missing } + + return $ CapacityInstance + { drawWith = DrawSettings + { withPlaceNames = not $ hidePlaceNames gc + , withSvgHighlighting = True + , withTransitionNames = not $ hideTransitionNames gc + , with1Weights = not $ hideWeight1 gc + , withGraphvizCommand = gl + } + , toFind = addMissingToCondition condition + , originalNet = original + , transformedNet = transformed + , complementMap = complementMap + , numberOfPlaces = places bc + , numberOfTransitions = transitions bc + , showSolution = Find.printSolution config + } + where + bc = Find.basicConfig config + gc = Pick.graphConfig config + +combinedCapacityInstance + :: (MonadThrow m, RandomGen g, MonadAlloy m, Net p n) + => CapacityConfig + -> Int + -> RandT g m (PetriLike CapacityNode String, p n String, PetriChangeList String, [(String, String)]) +combinedCapacityInstance = combinedCapacity + petriNetFindCapacity + Find.alloyConfig + +simpleCapacityTask + :: ( + MonadCache m, + MonadDiagrams m, + MonadGraphviz m, + MonadThrow m, + OutputCapable m + ) + => FilePath + -> CapacityInstance + -> LangM m +simpleCapacityTask = capacityTask + +capacityTask + :: ( + MonadCache m, + MonadDiagrams m, + MonadGraphviz m, + MonadThrow m, + OutputCapable m + ) + => FilePath + -> CapacityInstance + -> LangM m +capacityTask path task = do + paragraph $ translate $ do + english "Consider the following Petri net with capacities:" + german "Betrachten Sie folgendes Petrinetz mit Kapazitäten:" + image + $=<< cacheNetWithCapacity path (originalNet task) (drawWith task) + image + $=<< cacheNet path (transformedNet task) (drawWith task) + paragraph $ do + translate $ do + english [iii| + Given the not yet existing complement places that belong to the original places. With how many + tokens should they be generated, and how should they be connected to transitions, + so that the resulting Petri net without capacities is equivalent to the given Petri net with capacities? + |] + german [iii| + Gegeben der noch nicht existierenden, zu den Stellen gehörenden, Komplementstellen. Mit wie vielen Marken + sollten sie erstellt werden und wie sollten sie mit Transitionen verbunden werden, + sodass das resultierende Petrinetz ohne Kapazitäten äquivalent zu dem gegebenen Petrinetz mit Kapazitäten ist? + |] + translate $ do + english [iii| + State your answer by giving a tuple consisting of: + the complement places with their initial number of tokens, and + the flows connected to the complement places (incoming and outgoing). + #{" "}|] + german [iii| + Geben Sie Ihre Antwort in Form eines Tupels an, bestehend aus: + den Komplementstellen mit ihrer initialen Anzahl an Marken und + den Flüssen, die mit Komplementstellen verbunden sind (eingehend oder ausgehend). + #{" "}|] + translate $ do + english "The used mapping between complement places and places:" + german "Die genutzte Zuordnung zwischen Komplementstellen und Stellen:" + translate $ do + english $ intercalate ", " + ["Complement place " ++ cap ++ " to place " ++ add | (cap, add) <- complementMap task] + german $ intercalate ", " + ["Komplementstelle " ++ cap ++ " zu Stelle " ++ add | (cap, add) <- complementMap task] + translate $ do + english [i|. Stating |] + + german [i|. Die Angabe von |] + let ts :: ([(String, Int)], [(String, String, Int)]) + ts = ([("s1",2), ("s2",0)], [("t1","s1",1), ("t2","s1",1), ("s2","t2",2)]) + code $ show ts + translate $ do + english ("as answer would indicate that there are two complement places - s1 with 2 tokens " ++ + "and s2 with 0 tokens - and t1 points to s1 with a weight of 1, " ++ + "t2 points to s1 with a weight of 1 and s2 connects to t2 with a weight of 2. ") + german ("als Antwort würde bedeuten, dass es zwei Komplementstellen gibt - s1 mit 2 Token " ++ + "und s2 mit 0 Token - und t1 zeigt auf s1 mit einem Gewicht von 1, " ++ + "t2 zeigt auf s1 mit einem Gewicht von 1, und s2 ist mit t2 mit einem Gewicht von 2 verbunden. ") + translate $ do + english "The order of tuples within the lists does not matter here." + german "Die Reihenfolge der Tupel innerhalb der Listen spielt hierbei keine Rolle." + pure () + hoveringInformation True + pure () + +capacitySyntax + :: OutputCapable m + => CapacityInstance + -> ([(String, Int)], [(String, String, Int)]) + -> LangM' m () +capacitySyntax task (tokenChanges, flowChanges) = do + for_ tokenChanges assertTokenChanges + for_ flowChanges assertFlowChanges + pure () + where + assert = continueOrAbort True + + assertTokenChanges (p, tokens) = assert (isValidComplementPlace p && tokens >= 0) $ translate $ do + let p' = show (p, tokens) + english $ p' ++ " has a structurally correct form of a complement place?" + german $ p' ++ " hat eine strukturell korrekte Form einer Komplementstelle?" + + assertFlowChanges (src, tgt, weight) = assert (((isValidComplementPlace src && isValidTransition tgt) || + (isValidTransition src && isValidComplementPlace tgt)) && weight > 0) $ translate $ do + let t' = show (src, tgt, weight) + english $ t' ++ " has a structurally correct form of a flow?" + german $ t' ++ " hat eine strukturell korrekte Form eines Flusses?" + + isValidComplementPlace :: String -> Bool + isValidComplementPlace s = case s of + ('s':rest) -> maybe False (\x -> x >= 1 && x <= (numberOfPlaces task `div` 2)) (readMaybe rest) + _ -> False + + isValidTransition :: String -> Bool + isValidTransition t = case t of + ('t':rest) -> maybe False (\x -> x >= 1 && x <= numberOfTransitions task) (readMaybe rest) + _ -> False + +capacityEvaluation + :: (Monad m, OutputCapable m) + => CapacityInstance + -> ([(String, Int)], [(String, String, Int)]) + -> Rated m +capacityEvaluation task (tokenChanges, flowChanges) = do + let whatTokens = translations $ do + english "The indicated tuples are added complement places?" + german "Die angegebenen Tupel sind hinzugefügte Komplementstellen?" + let whatFlows = translations $ do + english "The indicated tuples are added flows?" + german "Die angegebenen Tupel sind hinzugefügte Flüsse?" + uncurry (printSolutionAndAssert True) + . first (fmap (DefiniteArticle,)) + $=<< unLangM $ liftA2 combineResults + (toFindEvaluationTupleList whatTokens withSol tokens tokenChanges) + (toFindEvaluationTupleList whatFlows withSol flows flowChanges) + + where + (tokens, flows) = capacitySolution task + withSol = showSolution task + combineResults (list1, points1) (list2, points2) = (combineLists list1 list2, points1 * points2) + combineLists :: Maybe String -> Maybe String -> Maybe String + combineLists = liftA2 (\string1 string2 -> string1 ++ "," ++ string2) + +capacitySolution :: CapacityInstance -> ([(String, Int)], [(String, String, Int)]) +capacitySolution task = (tokenChanges $ toFind task, flowChanges $ toFind task) + +combinedCapacity + :: (MonadThrow m, RandomGen g, MonadAlloy m, Net p n) + => (config -> String) + -> (config -> AlloyConfig) + -> config + -> Int + -> RandT g m (PetriLike CapacityNode String, p n String, PetriChangeList String, [(String, String)]) +combinedCapacity alloyF alloyC config segment = do + let is = Find.maxInstances (alloyC config) + list <- lift $ getInstances is (Find.timeout $ alloyC config) (alloyF config) + when (null $ drop segment list) + $ lift $ throwM NoInstanceAvailable + inst <- case fromIntegral <$> is of + Nothing -> randomInstance list + Just n -> do + x <- randomInSegment segment n + case drop x list of + x':_ -> return x' + [] -> randomInstance list + + lift $ findCapacityInstance inst + where + randomInstance list = do + n <- randomInSegment segment (1 + ((length list - segment - 1) `div` 4)) + return $ list !! n + +findCapacityInstance + :: (MonadThrow m, Net p n) + => AlloyInstance + -> m (PetriLike CapacityNode String, p n String, PetriChangeList String, [(String, String)]) +findCapacityInstance inst = do + (transformed, nameMap) <- + parseRenamedNet (singleSig "this" "Nodes" "") "flow" "tokens" inst + + original <- + parseNet (\inst2 -> do + pl <- singleSig "this" "givenPlaces" "" inst2 + tr <- singleSig "this" "givenTransitions" "" inst2 + return (Set.union pl tr)) "defaultFlow" "defaultTokens" inst + >>= (addCapacities inst >=> traverseNet (`BM.lookup` nameMap)) + + change <- parseChange inst + condition <- traverse (`BM.lookup` nameMap) (toChangeList change) + + complements <- doubleSig "this" "placesWithCapacity" "complement" inst + complementMap <- mapM (bimapM (`BM.lookup` nameMap) (`BM.lookup` nameMap)) (Set.toList complements) + + return (original, transformed, condition, complementMap) + +petriNetFindCapacity :: CapacityConfig -> String +petriNetFindCapacity CapacityConfig { + basicConfig, + advConfig, + maxCapacity, + newArrowsWithComplement, + oneMinCapacity, + distractors, + atMostActive + } + = petriNetFindCapacityAlloy + basicConfig + advConfig + maxCapacity + newArrowsWithComplement + oneMinCapacity + distractors + atMostActive + +parseCapacityPrec :: Int -> Parser Capacity +parseCapacityPrec _ = do + spaces + void $ char '(' + spaces + places <- parsePlacesWithInts + spaces + void $ char ',' + spaces + flows <- parseFlowTriples + spaces + void $ char ')' + return (Capacity (places, flows)) + where + parsePlacesWithInts = + char '[' *> parsePlaceWithInt `sepBy` (spaces *> char ',' <* spaces) <* char ']' + + parsePlaceWithInt = do + spaces + void $ char '(' + spaces + p <- parsePlacePrec 0 + spaces + void $ char ',' + spaces + n <- parseInt + spaces + void $ char ')' + return (p, n) + + parseFlowTriples = + char '[' *> parseFlowTriple `sepBy` (spaces *> char ',' <* spaces) <* char ']' + + parseFlowTriple = do + spaces + void $ char '(' + spaces + a <- parseNodeC + spaces + void $ char ',' + spaces + b <- parseNodeC + spaces + void $ char ',' + spaces + n <- parseInt + spaces + void $ char ')' + return (a, b, n) + + parseInt = read <$> many1 digit + + parseNodeC :: Parser String + parseNodeC = do + tag <- optionMaybe (char 's') + case tag of + Just _ -> do + Reach.Place n <- parsePlacePrec 0 + return $ show n + Nothing -> do + Reach.Transition n <- parseTransitionPrec 0 + return $ show n + +petriNetFindCapacityAlloy + :: BasicConfig + -> AdvConfig + -> Int + -> (Int, Int) + -> Int + -> (Int, Int) + -> Maybe Int + -> String +petriNetFindCapacityAlloy basicC advConfig maxCapacity newArrowsWithComplement oneMinCapacity distractors atMostActive + = [i|module PetriNetCapacity + +#{modulePetriSignature} +#{modulePetriAdditions} +#{moduleHelpers} +#{modulePetriConcepts} +#{modulePetriConstraints} + +sig placesWithCapacity extends givenPlaces +{ + capacity : one Int, + complement : disj one addedPlaces +} +{ + capacity > 0 + capacity =< #{maxCapacity} + complement.@tokens = minus[capacity, tokens] +} + +fact { + no addedTransitions + no givenPlaces.tokenChange + no givenPlaces.flowChange + Transitions.flowChange.Int in addedPlaces + addedPlaces.flowChange.Int in Transitions +} + +pred #{capacityPredicateName}[#{activated} : set Transitions] { + #{defaultConstraintsAtLeastZero} + #{compAdvConstraints True advConfig} + + all t : Transitions, p : givenPlaces | + let n = minus[t.flow[p], p.flow[t]] | + n < 0 implies (t.flow[p.complement] = minus[0, n] and no p.complement.flow[t]) + else + n > 0 implies (p.complement.flow[t] = n and no t.flow[p.complement]) + else + no p.complement.flow[t] and no t.flow[p.complement] + + all p : placesWithCapacity, w : p.flow[Transitions] + Transitions.flow[p] | p.capacity >= w + + all p : addedPlaces | some p.flowChange.Int or some p.~(flowChange.Int) + + #{newArrowsWithComplementConstraints newArrowsWithComplement} + #{oneMinCapacityConstraints oneMinCapacity} + #{distractorsConstraints distractors} + +} + +run #{capacityPredicateName} for exactly #{places basicC} givenPlaces, exactly #{places basicC} addedPlaces, +exactly #{transitions basicC} Transitions, #{petriScopeBitWidth (basicConfigBitWidthInput basicC ++ [snd newArrowsWithComplement, maxCapacity])} Int +|] + where + activated = skolemName + defaultConstraintsAtLeastZero = + enforceConstraints True Nothing undefined (basicC { atLeastActive = 0 }) + ++ + "#" ++ activated ++ " >= " ++ show (atLeastActive basicC) ++ "\n" + ++ + (case atMostActive of + Nothing -> "" + Just n -> " #" ++ activated ++ " <= " ++ show n ++ "\n") + ++ + " theActivatedTransitions[" ++ activated ++ "]" + newArrowsWithComplementConstraints (minNewArrowsMin, minNewArrowsMax) = + "let newArrows = #flowChange | newArrows >= " ++ show minNewArrowsMin ++ + " and newArrows =< " ++ show minNewArrowsMax + oneMinCapacityConstraints 1 = "" + oneMinCapacityConstraints oneMinCap = + [i|some p : placesWithCapacity | p.capacity >= #{oneMinCap}|] + distractorsConstraints (distractorsMin, distractorsMax) = + "let distractors = #{t : Transitions | activatedDefault[t] and t not in " ++ activated ++ "} |\n" ++ + " distractors >= " ++ show distractorsMin ++ " and distractors =< " ++ show distractorsMax + +capacityPredicateName :: String +capacityPredicateName = "showCapacity" + +skolemName :: String +skolemName = "activatedTrans" + +checkCapacityConfigs :: CapacityConfig -> Maybe String +checkCapacityConfigs CapacityConfig { + basicConfig, + maxCapacity, + newArrowsWithComplement, + oneMinCapacity, + distractors, + atMostActive, + graphConfig + } + = prohibitHidePlaceNames graphConfig + <|> prohibitHideTransitionNames graphConfig + <|> checkBasicConfig [snd newArrowsWithComplement, maxCapacity] basicConfig + <|> prohibitPatchworkRenderer graphConfig + <|> checkCapacityConfig basicConfig maxCapacity newArrowsWithComplement oneMinCapacity distractors atMostActive + <|> checkActivatedTransitionsConfig basicConfig atMostActive + +checkCapacityConfig :: BasicConfig -> Int -> (Int, Int) -> Int -> (Int, Int) -> Maybe Int -> Maybe String +checkCapacityConfig BasicConfig { + places, + transitions, + atLeastActive, + maxTokensPerPlace, + maxFlowPerEdge, + isConnected + } + maxCapacity + newArrowsWithComplement + oneMinCapacity + distractors + atMostActive + | maxCapacity < maxFlowPerEdge + = Just "'maxCapacity' can not be too low for flow weights." + | maxCapacity < maxTokensPerPlace + = Just "The starting tokens can not exceed 'maxCapacity'." + | atLeastActive == 0 + = Just "At least one transition has to be activated." + | uncurry (>) newArrowsWithComplement + = Just "The first element of 'newArrowsWithComplement' can not be higher than the second element." + | fst newArrowsWithComplement < places + = Just "At least one flow has to be connected to each complement place." + | snd newArrowsWithComplement > 2 * transitions * places + = Just "'newArrowsWithComplement' is set unreasonably high, given the number of transitions and places." + | oneMinCapacity <= 0 + = Just "'oneMinCapacity' has to be positive." + | oneMinCapacity > maxCapacity + = Just "'oneMinCapacity' can not be higher than 'maxCapacity'." + | uncurry (>) distractors + = Just "The first element of 'distractors' can not be higher than the second element." + | fst distractors < 0 + = Just "The first element of 'distractors' can not be negative." + | fst distractors > transitions - fromMaybe transitions atMostActive + = Just "'fst distractors' is set unreasonably high, given atMostActive." + | snd distractors > transitions - atLeastActive + = Just "'snd distractors' is set unreasonably high, given atLeastActive." + | isConnected /= Just True + = Just "The Petri net must be connected." + | otherwise + = Nothing + +defaultCapacityInstance :: CapacityInstance +defaultCapacityInstance = CapacityInstance { + drawWith = DrawSettings { + withPlaceNames = True, + withSvgHighlighting = True, + withTransitionNames = True, + with1Weights = False, + withGraphvizCommand = Circo + }, +toFind = ChangeList { + tokenChanges = [("s1", 1), ("s2", 0)] + , flowChanges = [("s1", "t2", 1), ("t1", "s1", 1), ("t2", "s2", 1), ("s2", "t1", 1), ("t3", "s2", 1)] + }, + originalNet = PetriLike { + allNodes = M.fromList [ + ("s3",CapacityPlace {initial = 1, capacity = 2, flowOut = M.fromList [("t1",1)]}), + ("s4",CapacityPlace {initial = 1, capacity = 1, flowOut = M.fromList [("t2",1),("t3",1)]}), + ("t1",CapacityTransition {flowOut = M.fromList [("s4",1)]}), + ("t2",CapacityTransition {flowOut = M.fromList [("s3",1)]}), + ("t3",CapacityTransition {flowOut = M.empty}) + ] + }, + transformedNet = PetriLike { + allNodes = M.fromList [ + ("s1",SimplePlace {initial = 1, flowOut = M.fromList [("t2",1)]}), + ("s2",SimplePlace {initial = 0, flowOut = M.fromList [("t1",1)]}), + ("s3",SimplePlace {initial = 1, flowOut = M.fromList [("t1",1)]}), + ("s4",SimplePlace {initial = 1, flowOut = M.fromList [("t2",1),("t3",1)]}), + ("t1",SimpleTransition {flowOut = M.fromList [("s1",1),("s4",1)]}), + ("t2",SimpleTransition {flowOut = M.fromList [("s2",1),("s3",1)]}), + ("t3",SimpleTransition {flowOut = M.fromList [("s2",1)]}) + ] + }, + complementMap = [("s1", "s3"), ("s2", "s4")], + numberOfPlaces = 4, + numberOfTransitions = 3, + showSolution = False +} diff --git a/src/Modelling/PetriNet/Concurrency.hs b/src/Modelling/PetriNet/Concurrency.hs index 6394dfb54..dbd42cc27 100644 --- a/src/Modelling/PetriNet/Concurrency.hs +++ b/src/Modelling/PetriNet/Concurrency.hs @@ -62,8 +62,6 @@ import Modelling.PetriNet.Alloy ( modulePetriConcepts, modulePetriConstraints, modulePetriSignature, - petriScopeBitWidth, - petriScopeMaxSeq, signatures, skolemVariable, taskInstance, @@ -76,9 +74,10 @@ import Modelling.PetriNet.Diagram ( import Modelling.PetriNet.Find ( FindInstance (..), checkConfigForFind, - findInitial, + checkFindTwoActive, + findInitialTuple, findTaskInstance, - toFindEvaluation, + toFindEvaluationTuple, toFindSyntax, ) import Modelling.PetriNet.Parser ( @@ -110,6 +109,8 @@ import Modelling.PetriNet.Types ( SimpleNode (..), SimplePetriNet, allDrawSettings, + basicConfigBitWidthInput, + petriScopeBitWidth, transitionPairShow, ) @@ -210,7 +211,7 @@ findConcurrencyTask showInputHelp path task = do translate $ do english [i|Stating |] german [i|Die Angabe von |] - let ts = transitionPairShow findInitial + let ts = transitionPairShow findInitialTuple code $ show ts translate $ do let (t1, t2) = bimap show show ts @@ -228,6 +229,7 @@ findConcurrencyTask showInputHelp path task = do Die Reihenfolge der Transitionen innerhalb des Paars spielt hierbei keine Rolle. |] + pure () hoveringInformation True extra $ Find.addText task @@ -247,11 +249,11 @@ findConcurrencyEvaluation -> Rated m findConcurrencyEvaluation task x = do let what = translations $ do - english "are concurrently activated" - german "sind nebenläufig aktiviert" + english "The indicated transitions are concurrently activated?" + german "Die angegebenen Transitionen sind nebenläufig aktiviert?" uncurry (printSolutionAndAssert False) . first (fmap (DefiniteArticle,)) - $=<< unLangM $ toFindEvaluation what withSol concur x + $=<< unLangM $ toFindEvaluationTuple what withSol concur x where concur = findConcurrencySolution task withSol = Find.showSolution task @@ -447,10 +449,8 @@ petriNetConcurrencyAlloy basicC changeC specific #{modulePetriConcepts} #{modulePetriConstraints} -pred #{concurrencyPredicateName}[#{defaultActiveTrans}#{activated} : set Transitions, #{t1}, #{t2} : Transitions] { - \#Places = #{places basicC} - \#Transitions = #{transitions basicC} - #{compBasicConstraints activated basicC} +pred #{concurrencyPredicateName}[#{skolemSets}#{t1}, #{t2} : Transitions] { + #{compBasicConstraints True Nothing activated basicC} #{compChange changeC} #{sourceTransitionConstraints} no disj x,y : givenTransitions | concurrentDefault[x + y] @@ -460,14 +460,14 @@ pred #{concurrencyPredicateName}[#{defaultActiveTrans}#{activated} : set Transit #{compConstraints} } -run #{concurrencyPredicateName} for exactly #{petriScopeMaxSeq basicC} Nodes, #{petriScopeBitWidth basicC} Int +run #{concurrencyPredicateName} for exactly #{places basicC} Places, exactly #{transitions basicC} Transitions, #{petriScopeBitWidth (basicConfigBitWidthInput basicC)} Int |] where activated = "activatedTrans" activatedDefault = "defaultActiveTrans" compConstraints = either (const $ defaultConstraints activatedDefault basicC) - compAdvConstraints + (compAdvConstraints False) specific sourceTransitionConstraints | Left True <- specific = [i| @@ -475,11 +475,14 @@ run #{concurrencyPredicateName} for exactly #{petriScopeMaxSeq basicC} Nodes, #{ no t : Transitions | sourceTransitions[t]|] | otherwise = "" defaultActiveTrans - | isLeft specific = [i|#{activatedDefault} : set givenTransitions,|] + | isLeft specific = [i|#{activatedDefault} : set givenTransitions, |] | otherwise = "" sigs = signatures "given" (places basicC) (transitions basicC) t1 = transition1 t2 = transition2 + skolemSets + | atLeastActive basicC > 0 = [i|#{defaultActiveTrans}#{activated} : set Transitions, |] + | otherwise = "" concurrencyPredicateName :: String concurrencyPredicateName = "showConcurrency" @@ -503,8 +506,8 @@ It throws an error instead if unexpected behaviour occurs. -} parseConcurrency :: MonadThrow m => AlloyInstance -> m (Concurrent Object) parseConcurrency inst = do - t1 <- unscopedSingleSig inst concurrencyTransition1 "" - t2 <- unscopedSingleSig inst concurrencyTransition2 "" + t1 <- unscopedSingleSig concurrencyTransition1 "" inst + t2 <- unscopedSingleSig concurrencyTransition2 "" inst Concurrent <$> ((,) <$> asSingleton t1 <*> asSingleton t2) checkFindConcurrencyConfig :: FindConcurrencyConfig -> Maybe String @@ -514,7 +517,9 @@ checkFindConcurrencyConfig FindConcurrencyConfig { changeConfig, graphConfig } - = checkConfigForFind basicConfig changeConfig graphConfig + = + checkFindTwoActive basicConfig + <|> checkConfigForFind basicConfig changeConfig graphConfig <|> additionalCheck basicConfig advConfig where additionalCheck BasicConfig {..} AdvConfig {..} diff --git a/src/Modelling/PetriNet/Conflict.hs b/src/Modelling/PetriNet/Conflict.hs index 7c0098558..d063172cf 100644 --- a/src/Modelling/PetriNet/Conflict.hs +++ b/src/Modelling/PetriNet/Conflict.hs @@ -70,8 +70,6 @@ import Modelling.PetriNet.Alloy ( modulePetriConcepts, modulePetriConstraints, modulePetriSignature, - petriScopeBitWidth, - petriScopeMaxSeq, signatures, skolemVariable, taskInstance, @@ -84,10 +82,11 @@ import Modelling.PetriNet.Diagram ( import Modelling.PetriNet.Find ( FindInstance (..), checkConfigForFind, - findInitial, + checkFindTwoActive, + findInitialTuple, findTaskInstance, lToFind, - toFindEvaluation, + toFindEvaluationTuple, toFindSyntax, ) import Modelling.PetriNet.Parser ( @@ -126,7 +125,9 @@ import Modelling.PetriNet.Types ( SimpleNode (..), SimplePetriNet, allDrawSettings, + basicConfigBitWidthInput, lConflictPlaces, + petriScopeBitWidth, transitionPairShow, ) @@ -226,7 +227,7 @@ findConflictTask showInputHelp path task = do translate $ do english [i|Stating |] german [i|Die Angabe von |] - let ts = transitionPairShow findInitial + let ts = transitionPairShow findInitialTuple code $ show ts translate $ do let (t1, t2) = bimap show show ts @@ -278,7 +279,7 @@ findConflictPlacesEvaluation -> ConflictPlaces -> Rated m findConflictPlacesEvaluation task (conflict, ps) = - toFindEvaluation what withSol conf conflict $>>= \(ms, res) -> do + toFindEvaluationTuple what withSol conf conflict $>>= \(ms, res) -> do recoverFrom $ unless (null inducing || res == 0) $ do for_ ps' $ \x -> assert (x `elem` inducing) $ translate $ do let x' = show $ ShowPlace x @@ -306,8 +307,8 @@ findConflictPlacesEvaluation task (conflict, ps) = base = fromIntegral $ 2 + numberOfPlaces task size = fromIntegral . length what = translations $ do - english "have a conflict" - german "haben einen Konflikt" + english "The indicated transitions have a conflict?" + german "Die angegebenen Transitionen haben einen Konflikt?" findConflictPlacesSolution :: FindInstance n (PetriConflict p t) -> ((t, t), [p]) findConflictPlacesSolution task = @@ -516,10 +517,8 @@ petriNetConflictAlloy basicC changeC conflictC uniqueConflictP specific #{modulePetriConcepts} #{modulePetriConstraints} -pred #{conflictPredicateName}[#{p} : some Places,#{defaultActiveTrans}#{activated} : set Transitions, #{t1}, #{t2} : Transitions] { - \#Places = #{places basicC} - \#Transitions = #{transitions basicC} - #{compBasicConstraints activated basicC} +pred #{conflictPredicateName}[#{p} : some Places, #{skolemSets}#{t1}, #{t2} : Transitions] { + #{compBasicConstraints True Nothing activated basicC} #{compChange changeC} #{multiplePlaces uniqueConflictP} #{sourceTransitionConstraints} @@ -535,14 +534,14 @@ pred #{conflictPredicateName}[#{p} : some Places,#{defaultActiveTrans}#{activate #{compConstraints} } -run #{conflictPredicateName} for exactly #{petriScopeMaxSeq basicC} Nodes, #{petriScopeBitWidth basicC} Int +run #{conflictPredicateName} for exactly #{places basicC} Places, exactly #{transitions basicC} Transitions, #{petriScopeBitWidth (basicConfigBitWidthInput basicC)} Int |] where activated = "activatedTrans" activatedDefault = "defaultActiveTrans" compConstraints = either (const $ defaultConstraints activatedDefault basicC) - compAdvConstraints + (compAdvConstraints False) specific sourceTransitionConstraints | Left True <- specific = [i| @@ -579,7 +578,7 @@ run #{conflictPredicateName} for exactly #{petriScopeMaxSeq basicC} Nodes, #{pet let ps = common#{upperFirst which}Preconditions[t1, t2] | \#ps > 1 and all p : ps | p.#{tokens} >= p.#{flow}[t1] and p.#{tokens} >= p.#{flow}[t2]|] defaultActiveTrans - | isLeft specific = [i|#{activatedDefault} : set givenTransitions,|] + | isLeft specific = [i|#{activatedDefault} : set givenTransitions, |] | otherwise = "" multiplePlaces unique | unique == Just True @@ -592,6 +591,9 @@ run #{conflictPredicateName} for exactly #{petriScopeMaxSeq basicC} Nodes, #{pet sigs = signatures "given" (places basicC) (transitions basicC) t1 = transition1 t2 = transition2 + skolemSets + | atLeastActive basicC > 0 = [i|#{defaultActiveTrans}#{activated} : set Transitions, |] + | otherwise = "" conflictPredicateName :: String conflictPredicateName = "showConflict" @@ -621,9 +623,9 @@ It returns an error message instead if unexpected behaviour occurs. -} parseConflict :: MonadThrow m => AlloyInstance -> m (PetriConflict' Object) parseConflict inst = do - tc1 <- unscopedSingleSig inst conflictTransition1 "" - tc2 <- unscopedSingleSig inst conflictTransition2 "" - pc <- unscopedSingleSig inst conflictPlaces1 "" + tc1 <- unscopedSingleSig conflictTransition1 "" inst + tc2 <- unscopedSingleSig conflictTransition2 "" inst + pc <- unscopedSingleSig conflictPlaces1 "" inst PetriConflict' . flip Conflict (Set.toList pc) <$> ((,) <$> asSingleton tc1 <*> asSingleton tc2) @@ -673,7 +675,9 @@ checkFindConflictConfig FindConflictConfig { conflictConfig, graphConfig } - = checkConfigForFind basicConfig changeConfig graphConfig + = + checkFindTwoActive basicConfig + <|> checkConfigForFind basicConfig changeConfig graphConfig <|> checkConflictConfig basicConfig conflictConfig checkPickConflictConfig :: PickConflictConfig -> Maybe String diff --git a/src/Modelling/PetriNet/ConflictPlaces.hs b/src/Modelling/PetriNet/ConflictPlaces.hs index e078ba5f6..201706b4e 100644 --- a/src/Modelling/PetriNet/ConflictPlaces.hs +++ b/src/Modelling/PetriNet/ConflictPlaces.hs @@ -33,8 +33,10 @@ import Modelling.PetriNet.Conflict ( import Modelling.PetriNet.Find ( FindInstance (..), checkConfigForFind, + checkFindTwoActive, drawFindWith, - findInitial, + findInitialTuple, + prohibitHidePlaceNames, ) import Modelling.PetriNet.Diagram ( cacheNet, @@ -50,7 +52,6 @@ import Modelling.PetriNet.Types ( Conflict, DrawSettings (..), FindConflictConfig (..), - GraphConfig (..), Net, PetriConflict (..), PetriLike (..), @@ -169,7 +170,7 @@ Die Reihenfolge von Stellen innerhalb der Auflistung der den Konflikt verursache pure () conflictInitial :: ConflictPlaces -conflictInitial = (findInitial, [Place 0, Place 1]) +conflictInitial = (findInitialTuple, [Place 0, Place 1]) findConflictPlacesSyntax :: OutputCapable m @@ -229,16 +230,10 @@ checkFindConflictPlacesConfig FindConflictConfig { graphConfig } = prohibitHidePlaceNames graphConfig + <|> checkFindTwoActive basicConfig <|> checkConfigForFind basicConfig changeConfig graphConfig <|> checkConflictConfig basicConfig conflictConfig -prohibitHidePlaceNames :: GraphConfig -> Maybe String -prohibitHidePlaceNames gc - | hidePlaceNames gc - = Just "Place names are required for this task type." - | otherwise - = Nothing - defaultFindConflictPlacesInstance :: FindInstance SimplePetriNet Conflict defaultFindConflictPlacesInstance = FindInstance { drawFindWith = DrawSettings { diff --git a/src/Modelling/PetriNet/Diagram.hs b/src/Modelling/PetriNet/Diagram.hs index 0dfb3aa75..9cb65819f 100644 --- a/src/Modelling/PetriNet/Diagram.hs +++ b/src/Modelling/PetriNet/Diagram.hs @@ -9,13 +9,16 @@ Provides the ability to render Petri nets. -} module Modelling.PetriNet.Diagram ( cacheNet, + cacheNetWithCapacity, drawNet, + drawNetWithCapacity, getDefaultNet, getNet, isNetDrawable, ) where import qualified Diagrams.TwoD.GraphViz as GV (getGraph) +import qualified Data.Bimap as BM (lookup) import qualified Data.Map as M (foldlWithKey, lookupMin) import Capabilities.Cache (MonadCache, cache, short) @@ -30,12 +33,14 @@ import Modelling.Auxiliary.Diagrams ( ) import Modelling.PetriNet.Parser ( netToGr, - parseNet, - simpleRenameWith, + netToGrWithCapacity, + parseRenamedNet, + singleSig, ) import Modelling.PetriNet.Types ( + CapacityNode, DrawSettings (..), - Net (traverseNet, nodes), + Net (nodes), ) import Control.Monad.Catch ( @@ -106,6 +111,44 @@ cacheNet path pl drawSettings@DrawSettings {..} = ++ short withGraphvizCommand ++ ".svg" +cacheNetWithCapacity + :: ( + Data (p CapacityNode String), + MonadCache m, + MonadDiagrams m, + MonadGraphviz m, + MonadThrow m, + Net p CapacityNode, + Typeable p + ) + => FilePath + -- ^ a prefix to use for resulting files + -> p CapacityNode String + -- ^ the graph to draw + -> DrawSettings + -- ^ how to draw the graph + -> m FilePath +cacheNetWithCapacity path pl drawSettings@DrawSettings {..} = + cache path ext prefix pl $ \pl' -> do + dia <- drawNetWithCapacity pl' drawSettings + renderDiagram dia + where + prefix = + "petri-with-capacity-" + ++ petriType + ++ nodeType + petriType = dataTypeName . dataTypeOf $ pl + nodeType = maybe + "" + (('-' :) . dataTypeName . dataTypeOf . snd) + $ M.lookupMin $ nodes pl + ext = short withPlaceNames + ++ short withTransitionNames + ++ short with1Weights + ++ short withSvgHighlighting + ++ short withGraphvizCommand + ++ ".svg" + newtype UnknownPetriNetNodeException = CouldNotFindNodeWithinGraph String deriving Show @@ -147,45 +190,35 @@ isNetDrawable pl = handle (const (pure False) . id @GraphvizException) . (>> pure True) . drawNet pl +drawNetWithCapacity + :: (MonadDiagrams m, MonadGraphviz m, MonadThrow m, Net p CapacityNode) + => p CapacityNode String + -> DrawSettings + -> m (Diagram B) +drawNetWithCapacity pl drawSettings@DrawSettings {..} = do + gr <- either (throwM . CouldNotFindNodeWithinGraph) return + $ netToGrWithCapacity pl + graph <- layoutGraph withGraphvizCommand gr + preparedFont <- lin + return $ drawGraphWithCapacity drawSettings preparedFont graph + getNet :: (MonadThrow m, Net p n, Traversable t) => (AlloyInstance -> m (t Object)) -> AlloyInstance -> m (p n String, t String) getNet parseSpecial inst = do - (net, rename) <- - getNetWith "flow" "tokens" inst + (net, nameMap) <- parseRenamedNet (singleSig "this" "Nodes" "") "flow" "tokens" inst special <- parseSpecial inst - renamedSpecial <- traverse rename special + renamedSpecial <- traverse (`BM.lookup` nameMap) special return (net, renamedSpecial) getDefaultNet :: (MonadThrow m, Net p n) => AlloyInstance -> m (p n String) -getDefaultNet inst= fst <$> - getNetWith "defaultFlow" "defaultTokens" inst - -{-| -Returns a Petri net like graph using 'parseNet'. -It additionally parses another part of the instance. -All nodes are renamed using the 'simpleRenameWith' function. -The renaming is also applied to the additionally parsed instance. --} -getNetWith - :: (MonadThrow m, Net p n) - => String - -- ^ flow - -> String - -- ^ tokens - -> AlloyInstance - -- ^ the instance to parse - -> m (p n String, Object -> m String) -getNetWith f t inst = do - pl <- parseNet f t inst - let rename = simpleRenameWith pl - pl' <- traverseNet rename pl - return (pl', rename) +getDefaultNet = + fmap fst . parseRenamedNet (singleSig "this" "Nodes" "") "defaultFlow" "defaultTokens" {-| Obtain the Petri net like graph by drawing Nodes and connections between them @@ -225,6 +258,38 @@ drawGraph drawSettings@DrawSettings {..} preparedFont graph = edges labelOnly = fst +drawGraphWithCapacity + :: DrawSettings + -> PreparedFont Double + -> Gr (AttributeNode (String, Maybe Int, Maybe Integer)) (AttributeEdge Int) + -> Diagram B +drawGraphWithCapacity drawSettings@DrawSettings {..} preparedFont graph = + graphEdges' # frame 1 + where + (nodes', edges) = GV.getGraph graph + graphNodes' = M.foldlWithKey + (\g l p -> g + `atop` + drawNodeWithCapacity drawSettings preparedFont l p) + mempty + nodes' + graphEdges' = foldl + (\g (s, t, l, p) -> + let ls = labelOnly s + lt = labelOnly t + in g # drawEdge + (not with1Weights) + preparedFont + l + ls + lt + (nonEmptyPathBetween p ls lt g) + ) + graphNodes' + edges + + labelOnly (x, _, _) = x + {-| Nodes are either Places (having 'Just' tokens), or Transitions (having 'Nothing'). @@ -282,6 +347,68 @@ drawNode DrawSettings {..} preparedFont (l, Just i) p # translate (r2 (8 * sqrt(fromIntegral (i - 1)), 0)) # rotateBy (fromIntegral j / fromIntegral i) +drawNodeWithCapacity + :: DrawSettings + -> PreparedFont Double + -> (String, Maybe Int, Maybe Integer) + -- ^ a capacity node (the first part is used for its label) with a capacity + -> Point V2 Double + -> Diagram B +drawNodeWithCapacity DrawSettings {..} preparedFont (l, Nothing, cap) p = + place + (addTransitionName $ rect 20 20 # lwL 0.5 # named l # svgClass "rect" # additionalLabel <> capacityLabel) + p + where + additionalLabel + | withSvgHighlighting = id + | otherwise = svgClass $ ' ' : l + addTransitionName + | not withTransitionNames = id + | otherwise = (center (text' preparedFont 18 l) `atop`) + capacityLabel = maybe mempty (drawCapacity preparedFont) cap + +drawNodeWithCapacity DrawSettings {..} preparedFont (l, Just i, cap) p + | i == 0 && cap == Just 0 = + place (foldl' atop mempty tokens) p + | i < 5 = + place (foldl' atop label (tokens ++ [emptyPlace, capacityLabel])) p + | otherwise = + place (foldl' atop label + [ token # translate (r2 (spacer, 0)) + , text' preparedFont 20 (show i) # translate (r2 (-spacer,-4)) + , emptyPlace + , capacityLabel + ]) p + where + spacer = 9 + additionalLabel + | withSvgHighlighting = id + | otherwise = svgClass $ ' ' : l + emptyPlace = circle 20 # lwL 0.5 # named l # svgClass "node" # additionalLabel + label + | not withPlaceNames = mempty + | otherwise = center (text' preparedFont 18 l) + # translate (r2 (0, - (3 * spacer))) + # svgClass "nlabel" + tokenGrey = sRGB24 136 136 136 + token = circle 4.5 # lc tokenGrey # fc tokenGrey # lwL 0 # svgClass "token" + tokens = [placeToken j | j <- [1..i]] + placeToken j = token + # translate (r2 (8 * sqrt (fromIntegral (i - 1)), 0)) + # rotateBy (fromIntegral j / fromIntegral i) + capacityLabel = maybe mempty (drawCapacity preparedFont) cap + +drawCapacity + :: PreparedFont Double + -> Integer + -> Diagram B +drawCapacity fontC cap = + case cap of + 0 -> mempty + _ -> text' fontC 18 (show cap) + # translate (r2 (0, 25)) + # svgClass "capacity" + {-| Edges are drawn as arcs between nodes (identified by labels). -} diff --git a/src/Modelling/PetriNet/Find.hs b/src/Modelling/PetriNet/Find.hs index d25e97b7b..5aa260688 100644 --- a/src/Modelling/PetriNet/Find.hs +++ b/src/Modelling/PetriNet/Find.hs @@ -11,12 +11,19 @@ module Modelling.PetriNet.Find ( FindInstance (..), - checkFindBasicConfig, checkConfigForFind, - findInitial, + checkFindTwoActive, + findInitialList, + findInitialTuple, findTaskInstance, lToFind, + prohibitHidePlaceNames, + prohibitHideTransitionNames, + prohibitPatchworkRenderer, toFindEvaluation, + toFindEvaluationList, + toFindEvaluationTuple, + toFindEvaluationTupleList, toFindSyntax, ) where @@ -41,7 +48,9 @@ import Modelling.PetriNet.Types ( Net (..), checkBasicConfig, checkChangeConfig, + prohibitPatchworkRenderer, shuffleNames, + transitionListShow, transitionPairShow, ) @@ -67,6 +76,7 @@ import Control.Monad.Random ( RandomGen, ) import Control.Monad.Trans.Class (MonadTrans (lift)) +import Data.List (sort) import Data.Map (Map) import Language.Alloy.Call ( AlloyInstance, @@ -86,8 +96,11 @@ data FindInstance n a = FindInstance { makeLensesFor [("toFind", "lToFind")] ''FindInstance -findInitial :: (Transition, Transition) -findInitial = (Transition 0, Transition 1) +findInitialTuple :: (Transition, Transition) +findInitialTuple = (Transition 0, Transition 1) + +findInitialList :: [Transition] +findInitialList = [Transition 0, Transition 1] toFindSyntax :: OutputCapable m @@ -122,35 +135,77 @@ toFindEvaluation :: (Num a, OutputCapable m) => Map Language String -> Bool - -> (Transition, Transition) - -> (Transition, Transition) + -> (b -> b -> Bool) + -> (b -> String) + -> b + -> b -> LangM' m (Maybe String, a) -toFindEvaluation what withSol (ft, st) (fi, si) = do - let correct = ft == fi && st == si || ft == si && st == fi +toFindEvaluation what withSol isCorrect format correctValue inputValue = do + let correct = isCorrect correctValue inputValue points = if correct then 1 else 0 maybeSolutionString = if withSol - then Just $ show $ transitionPairShow (ft, st) + then Just $ format correctValue else Nothing assert correct $ translate $ do - english $ "The indicated transitions " ++ localise English what ++ "?" - german $ "Die angegebenen Transitionen " ++ localise German what ++ "?" + english $ localise English what + german $ localise German what pure (maybeSolutionString, points) where assert = continueOrAbort withSol -checkFindBasicConfig :: BasicConfig -> Maybe String -checkFindBasicConfig BasicConfig { atLeastActive } +toFindEvaluationTuple + :: (Num a, OutputCapable m) + => Map Language String + -> Bool + -> (Transition, Transition) + -> (Transition, Transition) + -> LangM' m (Maybe String, a) +toFindEvaluationTuple what withSol = + toFindEvaluation what withSol pairEquals (show . transitionPairShow) + where + pairEquals (ft, st) (fi, si) = + (ft == fi && st == si) || (ft == si && st == fi) + +toFindEvaluationList + :: (Num a, OutputCapable m) + => Map Language String + -> Bool + -> [Transition] + -> [Transition] + -> LangM' m (Maybe String, a) +toFindEvaluationList what withSol = + toFindEvaluation what withSol (\x y -> sort x == sort y) (show . transitionListShow) + +toFindEvaluationTupleList + :: (Num a, Ord b, OutputCapable m, Show b) + => Map Language String + -> Bool + -> [b] + -> [b] + -> LangM' m (Maybe String, a) +toFindEvaluationTupleList what withSol = + toFindEvaluation what withSol (\xs ys -> sort xs == sort ys) (show . sort) + +checkFindTwoActive :: BasicConfig -> Maybe String +checkFindTwoActive BasicConfig { atLeastActive } | atLeastActive < 2 = Just "The parameter 'atLeastActive' must be at least 2 to create the task." | otherwise = Nothing checkConfigForFind :: BasicConfig -> ChangeConfig -> GraphConfig -> Maybe String checkConfigForFind basic change graph = - checkFindBasicConfig basic - <|> prohibitHideTransitionNames graph - <|> checkBasicConfig basic + prohibitHideTransitionNames graph + <|> checkBasicConfig [] basic <|> checkChangeConfig basic change + <|> prohibitPatchworkRenderer graph + +prohibitHidePlaceNames :: GraphConfig -> Maybe String +prohibitHidePlaceNames gc + | hidePlaceNames gc + = Just "Place names are required for this task type." + | otherwise + = Nothing prohibitHideTransitionNames :: GraphConfig -> Maybe String prohibitHideTransitionNames gc diff --git a/src/Modelling/PetriNet/FindActivatedTransitions.hs b/src/Modelling/PetriNet/FindActivatedTransitions.hs new file mode 100644 index 000000000..866475b07 --- /dev/null +++ b/src/Modelling/PetriNet/FindActivatedTransitions.hs @@ -0,0 +1,414 @@ +{-# LANGUAGE ApplicativeDo #-} +{-# LANGUAGE DuplicateRecordFields #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE TupleSections #-} + +module Modelling.PetriNet.FindActivatedTransitions ( + checkActivatedTransitionsConfig, + checkFindActivatedTransitionsConfig, + defaultFindActivatedTransitionsInstance, + findActivatedTransitions, + findActivatedTransitionsEvaluation, + findActivatedTransitionsGenerate, + findActivatedTransitionsSolution, + findActivatedTransitionsSyntax, + findActivatedTransitionsTask, + parseActivatedTransitions, + petriNetFindActivatedTransitions, + simpleFindActivatedTransitionsTask, + ) where + +import qualified Modelling.PetriNet.Find as F (showSolution) +import qualified Modelling.PetriNet.Types as Find ( + FindActivatedTransitionsConfig (..), + ) +import qualified Data.Map as M ( + empty, + fromList, + ) +import qualified Data.Set as Set ( + toList, + ) + +import Capabilities.Alloy (MonadAlloy) +import Capabilities.Cache (MonadCache) +import Capabilities.Diagrams (MonadDiagrams) +import Capabilities.Graphviz (MonadGraphviz) +import Modelling.Auxiliary.Common ( + Object, + oneOf, + parseWith, + ) +import Modelling.Auxiliary.Output ( + hoveringInformation, + ) +import Modelling.PetriNet.Alloy ( + compAdvConstraints, + compBasicConstraints, + compChange, + moduleHelpers, + modulePetriAdditions, + modulePetriConcepts, + modulePetriConstraints, + modulePetriSignature, + skolemVariable, + taskInstance, + unscopedSingleSig, + ) +import Modelling.PetriNet.Diagram ( + cacheNet, + ) +import Modelling.PetriNet.Find ( + FindInstance (..), + checkConfigForFind, + findInitialList, + findTaskInstance, + toFindEvaluationList, + ) +import Modelling.PetriNet.Reach.Type ( + ShowTransition (ShowTransition), + Transition (Transition), + parseTransitionPrec, + ) +import Modelling.PetriNet.Types ( + ActivatedTransitions (ActivatedTransitions), + AdvConfig (..), + BasicConfig (..), + ChangeConfig (..), + DrawSettings (..), + FindActivatedTransitionsConfig (..), + GraphConfig (..), + Net, + PetriLike (PetriLike, allNodes), + SimpleNode (..), + SimplePetriNet, + basicConfigBitWidthInput, + checkActivatedSourceConfig, + petriScopeBitWidth, + transitionListShow, + ) + +import Control.Applicative ((<|>)) +import Control.Monad.Catch (MonadThrow) +import Control.OutputCapable.Blocks ( + ArticleToUse (DefiniteArticle), + ExtraText (..), + GenericOutputCapable (..), + LangM', + LangM, + OutputCapable, + Rated, + ($=<<), + continueOrAbort, + english, + german, + printSolutionAndAssert, + translate, + translations, + unLangM + ) +import Control.Monad.Random ( + RandT, + RandomGen, + evalRandT, + mkStdGen + ) +import Control.Monad.Trans (MonadTrans (lift)) +import Data.Bifunctor (first) +import Data.Data (Data, Typeable) +import Data.Foldable (for_) +import Data.GraphViz.Commands (GraphvizCommand (Circo)) +import Data.Maybe (isNothing) +import Data.String.Interpolate (i, iii) +import Language.Alloy.Call ( + AlloyInstance + ) + +findActivatedTransitionsGenerate + :: (MonadAlloy m, MonadThrow m, Net p n) + => FindActivatedTransitionsConfig + -> Int + -> Int + -> m (FindInstance (p n String) (ActivatedTransitions Transition)) +findActivatedTransitionsGenerate config segment seed = flip evalRandT (mkStdGen seed) $ do + (d, c) <- findActivatedTransitions config segment + gl <- oneOf $ graphLayouts gc + c' <- lift $ traverse + (parseWith parseTransitionPrec) + c + return $ FindInstance { + drawFindWith = DrawSettings { + withPlaceNames = not $ hidePlaceNames gc, + withSvgHighlighting = True, + withTransitionNames = not $ hideTransitionNames gc, + with1Weights = not $ hideWeight1 gc, + withGraphvizCommand = gl + }, + toFind = c', + net = d, + numberOfPlaces = places bc, + numberOfTransitions = transitions bc, + showSolution = Find.printSolution config, + addText = Find.extraText config + } + where + bc = Find.basicConfig config + gc = Find.graphConfig config + +simpleFindActivatedTransitionsTask + :: ( + MonadCache m, + MonadDiagrams m, + MonadGraphviz m, + MonadThrow m, + OutputCapable m + ) + => FilePath + -> FindInstance SimplePetriNet (ActivatedTransitions Transition) + -> LangM m +simpleFindActivatedTransitionsTask = findActivatedTransitionsTask + +findActivatedTransitionsTask + :: ( + Data (n String), + Data (p n String), + MonadCache m, + MonadDiagrams m, + MonadGraphviz m, + MonadThrow m, + Net p n, + OutputCapable m, + Typeable n, + Typeable p + ) + => FilePath + -> FindInstance (p n String) (ActivatedTransitions Transition) + -> LangM m +findActivatedTransitionsTask path task = do + paragraph $ translate $ do + english "Consider the following Petri net:" + german "Betrachten Sie folgendes Petrinetz:" + image + $=<< cacheNet path (net task) (drawFindWith task) + paragraph $ translate $ do + english [iii| + Which transitions are activated + under the initial marking? + |] + german [iii| + Welche Transitionen sind unter der Startmarkierung aktiviert? + |] + paragraph $ do + translate $ do + english [iii| + State your answer by giving a list of activated transitions. + #{" "}|] + german [iii| + Geben Sie Ihre Antwort durch Angabe einer Liste + von aktivierten Transitionen an. + #{" "}|] + translate $ do + english [i|Stating |] + german [i|Die Angabe von |] + let ts = transitionListShow findInitialList + code $ show ts + translate $ do + let ta = map show ts + english [iii| + #{" "}as answer would indicate that exactly the transitions #{ta} + are activated under the initial marking. + #{" "}|] + german [iii| + #{" "}als Antwort würde bedeuten, dass genau die Transitionen #{ta} + unter der Startmarkierung aktiviert sind. + #{" "}|] + translate $ do + english "The order of transitions within the list does not matter here." + german [iii| + Die Reihenfolge der Transitionen innerhalb + der Liste spielt hierbei keine Rolle. + |] + + pure () + hoveringInformation True + pure () + +findActivatedTransitionsSyntax + :: OutputCapable m + => FindInstance net (ActivatedTransitions Transition) + -> [Transition] + -> LangM' m () +findActivatedTransitionsSyntax task transitions = do + for_ transitions assertTransition + pure () + where + assert = continueOrAbort False + assertTransition t = assert (isValidTransition t) $ translate $ do + let t' = show $ ShowTransition t + english $ t' ++ " is a transition of the given Petri net?" + german $ t' ++ " ist eine Transition des gegebenen Petrinetzes?" + isValidTransition (Transition x) = x >= 1 && x <= numberOfTransitions task + +findActivatedTransitionsEvaluation + :: (Monad m, OutputCapable m) + => FindInstance net (ActivatedTransitions Transition) + -> [Transition] + -> Rated m +findActivatedTransitionsEvaluation task x = do + let what = translations $ do + english "The indicated transitions are activated?" + german "Die angegebenen Transitionen sind aktiviert?" + uncurry (printSolutionAndAssert True) + . first (fmap (DefiniteArticle,)) + $=<< unLangM $ toFindEvaluationList what withSol active x + where + active = findActivatedTransitionsSolution task + withSol = F.showSolution task + +findActivatedTransitionsSolution :: FindInstance net (ActivatedTransitions a) -> [a] +findActivatedTransitionsSolution task = active + where + ActivatedTransitions active = toFind task + +findActivatedTransitions + :: (MonadAlloy m, MonadThrow m, Net p n, RandomGen g) + => FindActivatedTransitionsConfig + -> Int + -> RandT + g + m + (p n String, ActivatedTransitions String) +findActivatedTransitions = taskInstance + findTaskInstance + petriNetFindActivatedTransitions + parseActivatedTransitions + Find.alloyConfig + +petriNetFindActivatedTransitions :: FindActivatedTransitionsConfig -> String +petriNetFindActivatedTransitions FindActivatedTransitionsConfig { + basicConfig, + advConfig, + changeConfig, + atMostActive + } + = petriNetActivatedTransitionsAlloy + basicConfig + changeConfig + atMostActive + advConfig + +parseActivatedTransitions :: MonadThrow m => AlloyInstance -> m (ActivatedTransitions Object) +parseActivatedTransitions inst = do + t <- unscopedSingleSig activatedTransitions "" inst + pure $ ActivatedTransitions (Set.toList t) + +petriNetActivatedTransitionsAlloy + :: BasicConfig + -> ChangeConfig + -> Maybe Int + -> AdvConfig + -> String +petriNetActivatedTransitionsAlloy basicC changeC atMost advConfig + = [i|module PetriNetFindActivatedTransitions + +#{modulePetriSignature} +#{modulePetriAdditions} +#{moduleHelpers} +#{modulePetriConcepts} +#{modulePetriConstraints} + +pred #{activePredicateName}[#{activated} : set Transitions] { + #{compBasicConstraints True atMost activated basicC} + #{compChange changeC} + #{compAdvConstraints False advConfig} + #{activatedConstraint basicC atMost} + no t : givenTransitions | activatedDefault[t] +} + +run #{activePredicateName} for exactly #{places basicC} Places, exactly #{transitions basicC} Transitions, #{petriScopeBitWidth (basicConfigBitWidthInput basicC)} Int +|] + where + activated = skolemName + activatedConstraint :: BasicConfig -> Maybe Int -> String + activatedConstraint BasicConfig{ atLeastActive } atMostActive + | atLeastActive == 0 && isNothing atMostActive + = [i|theActivatedTransitions[#{activated}]|] + | otherwise + = "" -- because in all other cases already compBasicConstraints emits that constraint + +activePredicateName :: String +activePredicateName = "showActivatedTransitions" + +activatedTransitions :: String +activatedTransitions = skolemVariable activePredicateName skolemName + +skolemName :: String +skolemName = "activatedTrans" + +checkFindActivatedTransitionsConfig :: FindActivatedTransitionsConfig -> Maybe String +checkFindActivatedTransitionsConfig FindActivatedTransitionsConfig { + basicConfig, + advConfig, + changeConfig, + atMostActive, + graphConfig + } + = checkConfigForFind basicConfig changeConfig graphConfig + <|> checkActivatedSourceConfig basicConfig advConfig + <|> checkAdvConfig advConfig atMostActive + <|> checkActivatedTransitionsConfig basicConfig atMostActive + +checkAdvConfig :: AdvConfig -> Maybe Int -> Maybe String +checkAdvConfig AdvConfig{ presenceOfSourceTransitions } atMostActive + | isNothing presenceOfSourceTransitions && atMostActive == Just 0 + -- no check for Just True necessary since already handled by checkActivatedSourceConfig + = Just "When atMostActive = 'Just 0', use presenceOfSourceTransitions = 'Just False'." + | otherwise + = Nothing + +checkActivatedTransitionsConfig :: BasicConfig -> Maybe Int -> Maybe String +checkActivatedTransitionsConfig BasicConfig { + atLeastActive, + transitions + } + atMostActive = + case atMostActive of + Just atMost + | atMost < 0 + -> Just "atMostActive must be non-negative." + | atMost == transitions + -> Just "When atMostActive equals the total number of transitions, it is redundant. Rather use atMostActive = 'Nothing' instead." + | atLeastActive > atMost + -> Just "atLeastActive must not be greater than atMostActive." + | transitions < atMost + -> Just "There must be at least as many transitions as atMostActive." + _ -> Nothing + +defaultFindActivatedTransitionsInstance :: FindInstance SimplePetriNet (ActivatedTransitions Transition) +defaultFindActivatedTransitionsInstance = FindInstance { + drawFindWith = DrawSettings { + withPlaceNames = False, + withSvgHighlighting = True, + withTransitionNames = True, + with1Weights = False, + withGraphvizCommand = Circo + }, + toFind = ActivatedTransitions [Transition 1, Transition 2], + net = PetriLike { + allNodes = M.fromList [ + ("s1",SimplePlace {initial = 2, flowOut = M.fromList [("t1",1),("t2",1)]}), + ("s2",SimplePlace {initial = 0, flowOut = M.empty}), + ("s3",SimplePlace {initial = 0, flowOut = M.empty}), + ("s4",SimplePlace {initial = 1, flowOut = M.fromList [("t1",1),("t3",2)]}), + ("t1",SimpleTransition {flowOut = M.fromList [("s2",2),("s3",2)]}), + ("t2",SimpleTransition {flowOut = M.fromList [("s3",1)]}), + ("t3",SimpleTransition {flowOut = M.fromList [("s3",1)]}) + ] + }, + numberOfPlaces = 4, + numberOfTransitions = 3, + showSolution = False, + addText = NoExtraText + } diff --git a/src/Modelling/PetriNet/MatchToMath.hs b/src/Modelling/PetriNet/MatchToMath.hs index 2160dde08..35bbc81b4 100644 --- a/src/Modelling/PetriNet/MatchToMath.hs +++ b/src/Modelling/PetriNet/MatchToMath.hs @@ -59,16 +59,19 @@ import Modelling.PetriNet.Alloy ( modulePetriConcepts, modulePetriConstraints, modulePetriSignature, - petriScopeBitWidth, - petriScopeMaxSeq, signatures, taskInstance, ) import Modelling.PetriNet.Diagram (cacheNet, isNetDrawable) import Modelling.PetriNet.LaTeX (toPetriMath) +import Modelling.PetriNet.Find ( + prohibitHidePlaceNames, + prohibitHideTransitionNames, + ) import Modelling.PetriNet.Parser ( parseChange, parseRenamedNet, + singleSig, ) import Modelling.PetriNet.Types ( AdvConfig, @@ -86,6 +89,8 @@ import Modelling.PetriNet.Types ( SimpleNode (..), SimplePetriLike, allDrawSettings, + basicConfigBitWidthInput, + checkActivatedSourceConfig, checkBasicConfig, checkChangeConfig, checkGraphLayouts, @@ -96,6 +101,8 @@ import Modelling.PetriNet.Types ( defaultGraphConfig, isPlaceNode, mapChange, + petriScopeBitWidth, + prohibitPatchworkRenderer, shuffleNames, ) @@ -369,7 +376,7 @@ matchToMath config segment = do return (net, math, changes') else matchToMath config segment where - parse = lift . parseRenamedNet "flow" "tokens" + parse = fmap fst . lift . parseRenamedNet (singleSig "this" "Nodes" "") "flow" "tokens" firstM :: Monad m => (a -> m b) -> (a, c) -> m (b, c) firstM f (p, c) = (,c) <$> f p @@ -392,7 +399,7 @@ mathInstance -> AlloyInstance -> RandT g m (String, p n String, Math) mathInstance config inst = do - petriLike <- lift $ parseRenamedNet "flow" "tokens" inst + petriLike <- fst <$> lift (parseRenamedNet (singleSig "this" "Nodes" "") "flow" "tokens" inst) petriLike' <- fst <$> shuffleNames petriLike let math = toPetriMath petriLike' let f = renderFalse petriLike' config @@ -568,24 +575,19 @@ checkGraphToMathConfig c@MathConfig { checkMathConfig :: MathConfig -> Maybe String checkMathConfig c@MathConfig { basicConfig, + advConfig, changeConfig, graphConfig, useDifferentGraphLayouts, wrongInstances - } = checkBasicConfig basicConfig - <|> prohibitHideNames graphConfig + } = checkBasicConfig [] basicConfig + <|> prohibitHidePlaceNames graphConfig + <|> prohibitHideTransitionNames graphConfig + <|> checkActivatedSourceConfig basicConfig advConfig <|> checkChangeConfig basicConfig changeConfig <|> checkConfig c <|> checkGraphLayouts useDifferentGraphLayouts wrongInstances graphConfig - -prohibitHideNames :: GraphConfig -> Maybe String -prohibitHideNames gc - | hidePlaceNames gc - = Just "Place names are required for this task type" - | hideTransitionNames gc - = Just "Transition names are required for this task type" - | otherwise - = Nothing + <|> prohibitPatchworkRenderer graphConfig checkConfig :: MathConfig -> Maybe String checkConfig MathConfig { @@ -619,16 +621,16 @@ fact{ no givenTransitions } -pred showNets[#{activated} : set Transitions] { - \#Places = #{places} - \#Transitions = #{transitions} - #{compBasicConstraints activated basicC} - #{compAdvConstraints advConfig} +pred showNets[#{skolemSet}] { + #{compBasicConstraints True Nothing activated basicC} + #{compAdvConstraints False advConfig} } -run showNets for exactly #{petriScopeMaxSeq basicC} Nodes, #{petriScopeBitWidth basicC} Int +run showNets for exactly #{places} Places, exactly #{transitions} Transitions, #{petriScopeBitWidth (basicConfigBitWidthInput basicC)} Int |] where - activated = "activatedTrans" + (skolemSet, activated) + | atLeastActive basicC > 0 = ([i|#{activated} : set Transitions|], "activatedTrans") + | otherwise = ("", undefined) renderFalse :: Net p n => p n String -> MathConfig -> String renderFalse @@ -640,28 +642,27 @@ renderFalse #{modulePetriConcepts} #{modulePetriConstraints} -#{places} -#{transitions} +#{thePlaces} +#{theTransitions} fact{ #{initialMark} #{defaultFlow} } -pred showFalseNets[#{activated} : set Transitions]{ - #{compBasicConstraints activated basicConfig} - #{compAdvConstraints advConfig} +pred showFalseNets[#{skolemSet}]{ + #{compBasicConstraints True Nothing activated basicConfig} + #{compAdvConstraints False advConfig} #{compChange changeConfig} } -run showFalseNets for exactly #{petriScopeMaxSeq basicConfig} Nodes, #{petriScopeBitWidth basicConfig} Int +run showFalseNets for exactly #{places basicConfig} Places, exactly #{transitions basicConfig} Transitions, #{petriScopeBitWidth (basicConfigBitWidthInput basicConfig)} Int |] where allNodes = nodes net (ps, ts) = M.partition isPlaceNode allNodes - activated = "activatedTrans" - places = unlines [extendLine p "givenPlaces" | p <- M.keys ps] - transitions = unlines [extendLine t "givenTransitions" | t <- M.keys ts] + thePlaces = unlines [extendLine p "givenPlaces" | p <- M.keys ps] + theTransitions = unlines [extendLine t "givenTransitions" | t <- M.keys ts] initialMark = M.foldrWithKey (\k -> (++) . tokenLine k) "" $ initialTokens <$> ps defaultFlow = M.foldrWithKey (\k _ -> (printFlow k ++)) "" allNodes printFlow :: String -> String @@ -680,6 +681,9 @@ run showFalseNets for exactly #{petriScopeMaxSeq basicConfig} Nodes, #{petriScop |] flowLine from to (Just f) = [i| #{from}.defaultFlow[#{to}] = #{f} |] + (skolemSet, activated) + | atLeastActive basicConfig > 0 = ([i|#{activated} : set Transitions|], "activatedTrans") + | otherwise = ("", undefined) defaultGraphToMathInstance :: GraphToMathInstance defaultGraphToMathInstance = MatchInstance { diff --git a/src/Modelling/PetriNet/Parser.hs b/src/Modelling/PetriNet/Parser.hs index f72192a05..9ed379991 100644 --- a/src/Modelling/PetriNet/Parser.hs +++ b/src/Modelling/PetriNet/Parser.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE RecordWildCards #-} {-| A module for parsing Petri Alloy instances into Haskell representations defined @@ -8,13 +9,16 @@ of graphs which are similar to Petri nets. -} module Modelling.PetriNet.Parser ( NoSingletonException (..), + addCapacities, asSingleton, - convertPetri, + doubleSig, netToGr, + netToGrWithCapacity, parseChange, parseNet, parseRenamedNet, - simpleNameMap, simpleRename, simpleRenameWith, + singleSig, + simpleNameMap, simpleRename, ) where import qualified Modelling.PetriNet.Types as PN ( @@ -28,22 +32,28 @@ import qualified Data.Set as Set ( Set, findMin, fromList, lookupMin, null, size, toList, ) import qualified Data.Map.Lazy as Map ( + alter, + empty, findIndex, foldlWithKey', foldrWithKey, lookup, ) +import Data.Maybe (fromMaybe) import Modelling.Auxiliary.Common (Object (Object, oName, oIndex), toMap) import Modelling.PetriNet.Types ( + CapacityNode (..), Net (emptyNet, outFlow, alterFlow, alterNode, traverseNet), - Petri, PetriChange (..), + PetriLike (..), PetriNode (..), + maybeCapacity, maybeInitial, - petriLikeToPetri, ) +import GHC.Num (integerFromInt) + import Control.Arrow (second) import Control.Monad.Catch (Exception, MonadThrow (throwM)) import Data.Bimap (Bimap) @@ -63,60 +73,42 @@ import Language.Alloy.Call ( ) {-| -Given the name of a flow set and a token set the given alloy instance is parsed -to a 'Net' graph and a 'Petri' is returned if the instance is indeed a -valid Petri net (after applying 'petriLikeToPetri'). --} -convertPetri - :: MonadThrow m - => String -- ^ the name of the flow set - -> String -- ^ the name of the token set - -> AlloyInstance -- ^ the Petri net 'AlloyInstance' - -> m Petri -convertPetri f t inst = do - p <- parseNet f t inst - petriLikeToPetri p - -{-| -Parse a 'Net' graph from an 'AlloyInstance' given the instances flow and -token set names. -And return an already renamed Petri net. +Parse a 'Net' graph from an 'AlloyInstance', using a certain node set accessor, +and given the instance's flow and token set names. +Return an already renamed Petri net, along with the renaming map. -} parseRenamedNet :: (MonadThrow m, Net p n) - => String + => (AlloyInstance -> m (Set Object)) + -> String -> String -> AlloyInstance - -> m (p n String) -parseRenamedNet flowSetName tokenSetName inst = do - petriLike <- parseNet flowSetName tokenSetName inst - let rename = simpleRenameWith petriLike - traverseNet rename petriLike - -{-| -Transform a given value into a 'String' by replacing it according to the -'simpleNameMap' retrieved by the given 'Net'. --} -simpleRenameWith :: (MonadThrow m, Net p n, Ord a) => p n a -> a -> m String -simpleRenameWith petriLike x = do + -> m (p n String, Bimap Object String) +parseRenamedNet getNodes flowSetName tokenSetName inst = do + petriLike <- parseNet getNodes flowSetName tokenSetName inst let nameMap = simpleNameMap petriLike - BM.lookup x nameMap + net <- traverseNet (`BM.lookup` nameMap) petriLike + return (net, nameMap) {-| -Parse a `Net' graph from an 'AlloyInstance' given the instances flow and -token set names. +Parse a 'Net' graph from an 'AlloyInstance', using a certain node set accessor, +and given the instance's flow and token set names. -} parseNet :: (MonadThrow m, Net p n) - => String -- ^ the name of the flow set + => (AlloyInstance -> m (Set Object))-- ^ how to get the relevant node set + -> String -- ^ the name of the flow set -> String -- ^ the name of the token set -> AlloyInstance -- ^ the Petri net 'AlloyInstance' -> m (p n Object) -parseNet flowSetName tokenSetName inst = do - nodes <- singleSig inst "this" "Nodes" "" - rawTokens <- doubleSig inst "this" "Places" tokenSetName +parseNet getNodes flowSetName tokenSetName inst = do + nodes <- getNodes inst + + rawTokens <- doubleSig "this" "Places" tokenSetName inst let tokens = relToMap (second oIndex) rawTokens - flow <- tripleSig inst "this" "Nodes" flowSetName + + flow <- tripleSig "this" "Nodes" flowSetName inst + return . foldrFlip (\(x, y, z) -> alterFlow x (oIndex z) y) flow . foldrFlip @@ -126,6 +118,32 @@ parseNet flowSetName tokenSetName inst = do where foldrFlip f = flip $ foldr f +addCapacities + :: MonadThrow m + => AlloyInstance + -> PetriLike CapacityNode Object + -> m (PetriLike CapacityNode Object) +addCapacities inst net = do + nodes <- singleSig "this" "placesWithCapacity" "" inst + + rawCapacity <- doubleSig "this" "placesWithCapacity" "capacity" inst + + let capacities = relToMap (second (integerFromInt . oIndex)) rawCapacity + + return $ foldr (\x -> updateCapacity x $ Map.lookup x capacities >>= Set.lookupMin) net nodes + +updateCapacity + :: Object + -> Maybe Integer + -> PetriLike CapacityNode Object + -> PetriLike CapacityNode Object +updateCapacity x y (PetriLike ns) = + PetriLike $ Map.alter updateCapacity' x ns + where + updateCapacity' Nothing = Just $ CapacityPlace (fromMaybe undefined y) 0 Map.empty + updateCapacity' (Just (CapacityPlace _ t o)) = Just $ CapacityPlace (fromMaybe undefined y) t o + updateCapacity' (Just (CapacityTransition o)) = Just $ CapacityTransition o + relToMap :: (Ord b, Ord c) => (a -> (b, c)) -> Set a -> Map b (Set c) relToMap f = toMap . Set.fromList . map f . Set.toList @@ -153,8 +171,8 @@ On error a 'Left' error message will be returned. -} parseChange :: MonadThrow m => AlloyInstance -> m (PetriChange Object) parseChange inst = do - flow <- tripleSig inst "this" "Nodes" "flowChange" - token <- doubleSig inst "this" "Places" "tokenChange" + flow <- tripleSig "this" "Nodes" "flowChange" inst + token <- doubleSig "this" "Places" "tokenChange" inst let tokenMap = relToMap (second oIndex) token tokenChange <- asSingleton `mapM` tokenMap let flowMap = relToMap tripleToOut flow @@ -187,35 +205,35 @@ asSingleton s singleSig :: MonadThrow m - => AlloyInstance - -> String + => String -> String -> String + -> AlloyInstance -> m (Set.Set Object) -singleSig inst st nd rd = do +singleSig st nd rd inst = do sig <- lookupSig (scoped st nd) inst getSingleAs rd (return .: Object) sig doubleSig :: MonadThrow m - => AlloyInstance - -> String + => String -> String -> String + -> AlloyInstance -> m (Set.Set (Object,Object)) -doubleSig inst st nd rd = do +doubleSig st nd rd inst = do sig <- lookupSig (scoped st nd) inst let obj = return .: Object getDoubleAs rd obj obj sig tripleSig :: MonadThrow m - => AlloyInstance - -> String + => String -> String -> String + -> AlloyInstance -> m (Set.Set (Object,Object,Object)) -tripleSig inst st nd rd = do +tripleSig st nd rd inst = do sig <- lookupSig (scoped st nd) inst let obj = return .: Object getTripleAs rd obj obj obj sig @@ -263,3 +281,21 @@ netToGr petriLike = do indexOf x = Map.findIndex x $ PN.nodes petriLike convertEdge source target flow rs = (indexOf source, indexOf target, flow) : rs + +netToGrWithCapacity + :: (Monad m, Net p CapacityNode, Ord a) + => p CapacityNode a + -> m (Gr (a, Maybe Int, Maybe Integer) Int) +netToGrWithCapacity petriLike = do + nodes <- Map.foldrWithKey convertNode (return []) $ PN.nodes petriLike + let edges = Map.foldrWithKey convertTransition [] $ PN.nodes petriLike + return $ mkGraph nodes edges + where + convertNode k x ns = do + ns' <- ns + return $ (indexOf k, (k, maybeInitial x, maybeCapacity x)):ns' + convertTransition k _ ns = + Map.foldrWithKey (convertEdge k) ns $ outFlow k petriLike + indexOf x = Map.findIndex x $ PN.nodes petriLike + convertEdge source target flow rs = + (indexOf source, indexOf target, flow) : rs diff --git a/src/Modelling/PetriNet/Pick.hs b/src/Modelling/PetriNet/Pick.hs index 97071b7c7..d10602c2e 100644 --- a/src/Modelling/PetriNet/Pick.hs +++ b/src/Modelling/PetriNet/Pick.hs @@ -55,6 +55,7 @@ import Modelling.PetriNet.Types ( checkChangeConfig, checkGraphLayouts, placeNames, + prohibitPatchworkRenderer, transitionNames, ) @@ -218,6 +219,7 @@ checkConfigForPick -> GraphConfig -> Maybe String checkConfigForPick useDifferent numWrongInstances basic change graph - = checkBasicConfig basic + = checkBasicConfig [] basic <|> checkChangeConfig basic change <|> checkGraphLayouts useDifferent numWrongInstances graph + <|> prohibitPatchworkRenderer graph diff --git a/src/Modelling/PetriNet/PickMistake.hs b/src/Modelling/PetriNet/PickMistake.hs new file mode 100644 index 000000000..4bbc032f4 --- /dev/null +++ b/src/Modelling/PetriNet/PickMistake.hs @@ -0,0 +1,349 @@ +{-# LANGUAGE ApplicativeDo #-} +{-# Language DuplicateRecordFields #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# Language QuasiQuotes #-} + +module Modelling.PetriNet.PickMistake ( + checkMistakeConfig, + checkPickMistakeConfig, + defaultPickMistakeInstance, + petriNetPickMistake, + pickMistake, + pickMistakeGenerate, + pickMistakeTask, + simplePickMistakeTask, + ) where + +import qualified Modelling.PetriNet.Types as Pick ( + PickMistakeConfig (..), + ) + +import qualified Data.Map as M ( + empty, + fromList, + ) + +import Capabilities.Alloy (MonadAlloy) +import Capabilities.Cache (MonadCache) +import Capabilities.Diagrams (MonadDiagrams) +import Capabilities.Graphviz (MonadGraphviz) +import Modelling.Auxiliary.Output ( + hoveringInformation, + ) +import Modelling.PetriNet.Alloy ( + compBasicConstraints, + compChange, + defaultConstraints, + moduleHelpers, + modulePetriConcepts, + modulePetriConstraints, + modulePetriSignature, + signatures, + taskInstance, + ) +import Modelling.PetriNet.Pick ( + PickInstance (..), + checkConfigForPick, + pickGenerate, + pickTaskInstance, + renderPick, + wrong, -- note that "wrong" in the context of the current module means + wrongInstances, -- "not having been infused with a mistake" + ) +import Modelling.PetriNet.Types ( + BasicConfig (..), + ChangeConfig (..), + DrawSettings (..), + MistakeConfig (..), + Net (..), + PetriLike (PetriLike, allNodes), + PickMistakeConfig (..), + SimpleNode (..), + SimplePetriNet, + basicConfigBitWidthInput, + petriScopeBitWidth, + ) + +import Control.Applicative ((<|>)) +import Control.Monad.Catch (MonadCatch, MonadThrow) +import Control.OutputCapable.Blocks ( + ExtraText (..), + GenericOutputCapable (..), + LangM, + OutputCapable, + ($=<<), + english, + german, + translate, + ) +import Control.Monad.Random ( + RandT, + RandomGen, + ) +import Control.Monad.Trans (MonadTrans (lift)) +import Data.Data (Data, Typeable) +import Data.GraphViz.Commands (GraphvizCommand (Fdp)) +import Data.Functor.Const (Const(..)) +import Data.String.Interpolate (i, iii) + +pickMistakeGenerate + :: (MonadAlloy m, MonadCatch m, MonadDiagrams m, MonadGraphviz m, Net p n) + => PickMistakeConfig + -> Int + -> Int + -> m (PickInstance (p n String)) +pickMistakeGenerate = pickGenerate pickMistake gc ud ws et + where + gc = Pick.graphConfig + ud = Pick.useDifferentGraphLayouts + ws = Pick.printSolution + et = Pick.extraText + +simplePickMistakeTask + :: (MonadCache m, + MonadDiagrams m, + MonadGraphviz m, + MonadThrow m, + OutputCapable m + ) + => FilePath + -> PickInstance SimplePetriNet + -> LangM m +simplePickMistakeTask = pickMistakeTask + +pickMistakeTask + :: ( + Data (n String), + Data (p n String), + MonadCache m, + MonadDiagrams m, + MonadGraphviz m, + MonadThrow m, + Net p n, + OutputCapable m, + Typeable n, + Typeable p + ) + => FilePath + -> PickInstance (p n String) + -> LangM m +pickMistakeTask path task = do + paragraph $ translate $ do + english [iii| + Which of the following Petri net candidates is not correctly formed? + |] + german [iii| + Welcher der folgenden Petrinetzkandidaten ist nicht korrekt geformt? + |] + images show snd + $=<< renderPick path task + paragraph $ translate $ do + english [iii| + State your answer by giving the number of the Petri net candidate + that is syntactically incorrect. + #{" "}|] + german [iii| + Geben Sie Ihre Antwort durch Angabe der Nummer des Petrinetzkandidaten an, + der syntaktisch inkorrekt ist. + #{" "}|] + let plural = wrongInstances task > 1 + paragraph $ do + translate $ do + english [i|Stating |] + german [i|Die Angabe von |] + code "1" + translate $ do + english [iii| + #{" "}as answer would indicate that Petri net candidate 1 is incorrect (and the other + #{if plural then "ones are" else "one is"} at least syntactically correct). + |] + german $ [iii| + #{" "}als Antwort würde bedeuten, dass Petrinetzkandidat 1 + inkorrekt ist, während + #{" "} + |] + ++ (if plural + then "die anderen zumindest syntaktisch korrekt sind." + else "der andere zumindest syntaktisch korrekt ist.") + pure () + hoveringInformation True + pure () + + +pickMistake + :: (MonadAlloy m, MonadThrow m, Net p n, RandomGen g) + => PickMistakeConfig + -> Int + -> RandT + g + m + [(p n String, Maybe (Const () String))] +pickMistake = taskInstance + (\f -> lift . pickTaskInstance f) + petriNetPickMistake + (\_ -> return (Const ())) + Pick.alloyConfig + + +petriNetPickMistake :: PickMistakeConfig -> String +petriNetPickMistake PickMistakeConfig{ + basicConfig, + changeConfig, + mistakeConfig + } = + petriNetPickMistakeAlloy + basicConfig + changeConfig + mistakeConfig + +{-| +Generate code for PetriNet mistake tasks +-} +petriNetPickMistakeAlloy + :: BasicConfig + -> ChangeConfig + -> MistakeConfig + -> String +petriNetPickMistakeAlloy basicC changeC mistakeC + = [i|module PetriNetPickMistake + +#{modulePetriSignature} +#{sigs} +#{moduleHelpers} +#{modulePetriConcepts} +#{modulePetriConstraints} + +pred #{mistakePredicateName} { + #{compBasicConstraints False Nothing undefined basicC} + #{pickMistakeConstraints mistakeC} + #{compChange changeC} + #{defaultConstraints undefined basicC} + #{prohibitSelfLoops mistakeC} +} + +run #{mistakePredicateName} for #{petriScopeBitWidth (basicConfigBitWidthInput basicC)} Int +|] + where + sigs = signatures "given" (places basicC) (transitions basicC) + prohibitSelfLoops :: MistakeConfig -> String + prohibitSelfLoops MistakeConfig{ canHaveTransitionToTransition, canHavePlaceToPlace } + | canHaveTransitionToTransition && canHavePlaceToPlace + = [i|all n : Nodes | no n.flow[n]|] + | canHaveTransitionToTransition + = [i|all n : Transitions | no n.flow[n]|] + | canHavePlaceToPlace + = [i|all n : Places | no n.flow[n]|] + | otherwise + = "" + +mistakePredicateName :: String +mistakePredicateName = "showMistake" + +pickMistakeConstraints :: MistakeConfig -> String +pickMistakeConstraints MistakeConfig + { canHaveNegativeWeight, canHaveTransitionToTransition, canHavePlaceToPlace + } = falseInput + where + input :: [(Bool, String)] + input = [(canHaveNegativeWeight, "all w : Nodes.flow[Nodes] | w > 0"), + (canHaveTransitionToTransition, "Transitions.flow.Int in Places"), + (canHavePlaceToPlace, "Places.flow.Int in Transitions")] + falseMistakes = map snd (filter (not . fst) input) + + falseInput :: String + falseInput = + case falseMistakes of + [] -> "" + (x:xs) -> unlines (x : map (" " ++) xs) + +checkPickMistakeConfig :: PickMistakeConfig -> Maybe String +checkPickMistakeConfig PickMistakeConfig { + basicConfig, + changeConfig, + mistakeConfig, + graphConfig, + useDifferentGraphLayouts + } + = checkConfigForPick + useDifferentGraphLayouts + wrong + basicConfig + changeConfig + graphConfig + <|> checkMistakeConfig basicConfig changeConfig mistakeConfig + +checkMistakeConfig :: BasicConfig -> ChangeConfig -> MistakeConfig -> Maybe String +checkMistakeConfig BasicConfig { + places, + transitions, + atLeastActive + } + ChangeConfig { + flowChangeOverall + } + MistakeConfig { + canHaveNegativeWeight, + canHaveTransitionToTransition, + canHavePlaceToPlace + } + | not (canHaveNegativeWeight || canHaveTransitionToTransition || canHavePlaceToPlace) + = Just "At least one mistake must be enabled." + | atLeastActive /= 0 + = Just "atLeastActive has to be 0 in this task type." + | canHaveTransitionToTransition && transitions < 2 + = Just "At least two transitions are required for transition mistakes." + | canHavePlaceToPlace && places < 2 + = Just "At least two places are required for place mistakes." + | flowChangeOverall < 1 + = Just "flowChangeOverall must be at least 1 for mistakes." + | otherwise + = Nothing + +defaultPickMistakeInstance :: PickInstance SimplePetriNet +defaultPickMistakeInstance = PickInstance { + nets = M.fromList [ + (1,(False,( + PetriLike { + allNodes = M.fromList [ + ("s1",SimplePlace {initial = 3, flowOut = M.fromList [("t1",1),("t3",2)]}), + ("s2",SimplePlace {initial = 0, flowOut = M.empty}), + ("s3",SimplePlace {initial = 1, flowOut = M.fromList [("t2",1)]}), + ("s4",SimplePlace {initial = 1, flowOut = M.fromList [("t2",1)]}), + ("t1",SimpleTransition {flowOut = M.fromList [("s2",1),("s3",1)]}), + ("t2",SimpleTransition {flowOut = M.fromList [("s1",1)]}), + ("t3",SimpleTransition {flowOut = M.fromList [("s4",2)]}) + ] + }, + DrawSettings { + withPlaceNames = False, + withSvgHighlighting = True, + withTransitionNames = False, + with1Weights = False, + withGraphvizCommand = Fdp + } + ))), + (2,(True,( + PetriLike { + allNodes = M.fromList [ + ("s1",SimplePlace {initial = 3, flowOut = M.fromList [("t1",-1),("t3",2)]}), + ("s2",SimplePlace {initial = 0, flowOut = M.empty}), + ("s3",SimplePlace {initial = 1, flowOut = M.fromList [("t2",1)]}), + ("s4",SimplePlace {initial = 1, flowOut = M.fromList [("t2",1)]}), + ("t1",SimpleTransition {flowOut = M.fromList [("s2",1),("s3",1)]}), + ("t2",SimpleTransition {flowOut = M.fromList [("t1",1)]}), + ("t3",SimpleTransition {flowOut = M.fromList [("s4",2)]}) + ] + }, + DrawSettings { + withPlaceNames = False, + withSvgHighlighting = True, + withTransitionNames = False, + with1Weights = False, + withGraphvizCommand = Fdp + } + ))) + ], + showSolution = False, + addText = NoExtraText + } diff --git a/src/Modelling/PetriNet/Reach/Deadlock.hs b/src/Modelling/PetriNet/Reach/Deadlock.hs index 96ea96241..c0d12687a 100644 --- a/src/Modelling/PetriNet/Reach/Deadlock.hs +++ b/src/Modelling/PetriNet/Reach/Deadlock.hs @@ -302,7 +302,7 @@ defaultDeadlockConfig = numPlaces = 6, numTransitions = 6, Modelling.PetriNet.Reach.Deadlock.capacity = Unbounded, - graphLayouts = [Dot, Neato, TwoPi, Circo, Fdp, Sfdp, Osage, Patchwork], + graphLayouts = [Dot, Neato, TwoPi, Circo, Fdp, Sfdp, Osage], maxTransitionLength = 8, minTransitionLength = 8, transitionBehaviorConstraints = noTransitionBehaviorConstraints, diff --git a/src/Modelling/PetriNet/Reach/Reach.hs b/src/Modelling/PetriNet/Reach/Reach.hs index a42192f69..caa708945 100644 --- a/src/Modelling/PetriNet/Reach/Reach.hs +++ b/src/Modelling/PetriNet/Reach/Reach.hs @@ -586,7 +586,7 @@ defaultReachConfig = ReachConfig { numPlaces = 6, numTransitions = 6, Modelling.PetriNet.Reach.Reach.capacity = Unbounded, - graphLayouts = [Dot, Neato, TwoPi, Circo, Fdp, Sfdp, Osage, Patchwork], + graphLayouts = [Dot, Neato, TwoPi, Circo, Fdp, Sfdp, Osage], maxTransitionLength = 6, minTransitionLength = 6, maxPlacesChanged = 3, diff --git a/src/Modelling/PetriNet/Types.hs b/src/Modelling/PetriNet/Types.hs index ad889882d..3ad3d1991 100644 --- a/src/Modelling/PetriNet/Types.hs +++ b/src/Modelling/PetriNet/Types.hs @@ -20,9 +20,13 @@ The 'Modelling.PetriNet.Types' module defines basic type class instances and functions to work on and transform Petri net representations. -} module Modelling.PetriNet.Types ( + ActivatedTransitions (ActivatedTransitions), AdvConfig (..), AlloyConfig (..), BasicConfig (..), + Capacity (Capacity), + CapacityConfig (..), + CapacityNode (..), Change, ChangeConfig (..), Concurrent (..), @@ -30,14 +34,17 @@ module Modelling.PetriNet.Types ( ConflictConfig (..), Drawable, DrawSettings (..), + FindActivatedTransitionsConfig (..), FindConcurrencyConfig (..), FindConflictConfig (..), GraphConfig (..), InvalidPetriNetException (..), + MistakeConfig (..), Net (..), Node (..), Petri (..), PetriChange (..), + PetriChangeList (..), PetriConflict (..), PetriConflict' (..), PetriLike (..), @@ -45,10 +52,13 @@ module Modelling.PetriNet.Types ( PetriNode (..), PickConcurrencyConfig (..), PickConflictConfig (..), + PickMistakeConfig (..), SimpleNode (..), SimplePetriLike, SimplePetriNet, allDrawSettings, + basicConfigBitWidthInput, + checkActivatedSourceConfig, checkBasicConfig, checkChangeConfig, checkGraphLayouts, @@ -56,9 +66,12 @@ module Modelling.PetriNet.Types ( defaultAdvConfig, defaultAlloyConfig, defaultBasicConfig, + defaultCapacityConfig, defaultChangeConfig, + defaultFindActivatedTransitionsConfig, defaultFindConcurrencyConfig, defaultFindConflictConfig, + defaultPickMistakeConfig, defaultGraphConfig, defaultPickConcurrencyConfig, defaultPickConflictConfig, @@ -87,11 +100,16 @@ module Modelling.PetriNet.Types ( lTransitions, lUniqueConflictPlace, mapChange, + maybeCapacity, maybeInitial, petriLikeToPetri, + petriScopeBitWidth, placeNames, + prohibitPatchworkRenderer, shuffleNames, + toChangeList, transformNet, + transitionListShow, transitionNames, transitionPairShow, ) where @@ -114,6 +132,7 @@ import qualified Data.Map.Lazy as M ( mapKeys, member, null, + toList, size, ) import qualified Data.Set as S (empty, union) @@ -121,6 +140,7 @@ import qualified Data.Set as S (empty, union) import Autolib.Hash (Hashable) import Autolib.Reader (Reader) import Autolib.ToDoc (ToDoc) +import Capabilities.Alloy (maxBitWidth) import Modelling.Auxiliary.Common (lensRulesL) import Modelling.PetriNet.Reach.Type (Place, ShowTransition (ShowTransition)) import Modelling.Types () @@ -134,6 +154,7 @@ import Control.OutputCapable.Blocks (ExtraText (..)) import Data.Bimap (Bimap) import Data.Data (Data) import Data.GraphViz.Attributes.Complete (GraphvizCommand (..)) +import Data.List (intercalate) import Data.Map.Lazy (Map) import Data.Maybe (fromMaybe) import GHC.Generics (Generic) @@ -173,6 +194,18 @@ data PetriChange a = Change { } deriving (Eq, Generic, Hashable, Read, Reader, Show, ToDoc) +data PetriChangeList a = ChangeList { + tokenChanges :: [(a, Int)], + flowChanges :: [(a, a, Int)] +} deriving (Eq, Generic, Hashable, Show, Functor, Foldable, Reader, Traversable, ToDoc) + +toChangeList :: PetriChange a -> PetriChangeList a +toChangeList (Change tokenMap flowMap) = ChangeList { + tokenChanges = M.toList tokenMap, + flowChanges = [ (source, target, n) | (source, targets) <- M.toList flowMap + , (target, n) <- M.toList targets ] +} + {-| This function acts like 'fmap' on other 'Functor's. @@ -235,6 +268,12 @@ instance Bitraversable PetriConflict where newtype Concurrent a = Concurrent (a, a) deriving (Eq, Foldable, Functor, Generic, Hashable, Read, Reader, Show, ToDoc, Traversable) +newtype ActivatedTransitions a = ActivatedTransitions [a] + deriving (Functor, Foldable, Traversable, Generic, Read, Reader, Show, ToDoc) + +newtype Capacity = Capacity ([(Place, Int)], [(String, String, Int)]) + deriving (Generic, Read, Show) + class Show (n String) => PetriNode n where initialTokens :: n a -> Int @@ -350,6 +389,39 @@ instance PetriNode SimpleNode where traverseNode f (SimpleTransition o) = SimpleTransition <$> traverseKeyMap f o +data CapacityNode a = + CapacityPlace { + capacity :: Integer, + -- | max allowed token number of a 'CapacityNode' + initial :: Int, + flowOut :: Map a Int + } | + CapacityTransition { + flowOut :: Map a Int + } + deriving (Data, Eq, Generic, Hashable, Read, Reader, Show, ToDoc) + +instance PetriNode CapacityNode where + initialTokens CapacityPlace {initial} = initial + initialTokens CapacityTransition {} = + error "A CapacityTransition does not have initial tokens!" + + isPlaceNode CapacityPlace {} = True + isPlaceNode _ = False + + isTransitionNode CapacityTransition {} = True + isTransitionNode _ = False + + mapNode f (CapacityPlace c s o) = + CapacityPlace c s (M.mapKeys f o) + mapNode f (CapacityTransition o) = + CapacityTransition (M.mapKeys f o) + + traverseNode f (CapacityPlace c s o) = + CapacityPlace c s <$> traverseKeyMap f o + traverseNode f (CapacityTransition o) = + CapacityTransition <$> traverseKeyMap f o + {-| Returns 'Just' the 'initial' tokens of the given node, if it is a place 'PetriNode', otherwise it returns 'Nothing'. @@ -359,6 +431,10 @@ maybeInitial n | isPlaceNode n = Just $ initialTokens n | otherwise = Nothing +maybeCapacity :: CapacityNode a -> Maybe Integer +maybeCapacity CapacityPlace{capacity} = Just capacity +maybeCapacity _ = Nothing + {-| A specific traversal for 'Map's changing the keys rather than values. That is why, the result requires an 'Ord' instance. @@ -483,7 +559,7 @@ instance Net PetriLike Node where $ ns deleteNode x (PetriLike ns) = PetriLike - . adjustAll (updateNode id (M.delete x)) (M.keys . flowIn <$> n) + . adjustAll (updateNode id (M.delete x)) (M.keys . flowInN <$> n) . adjustAll (updateNode (M.delete x) id) (M.keys . flowOutN <$> n) . M.delete x $ ns @@ -551,6 +627,45 @@ updateSimpleNode g (SimpleTransition o) = SimpleTransition (g o) type SimplePetriLike = PetriLike SimpleNode type SimplePetriNet = SimplePetriLike String +instance Net PetriLike CapacityNode where + emptyNet = PetriLike M.empty + + flow x y = (M.lookup y . flowOutCN) <=< (M.lookup x . allNodes) + + nodes = allNodes + + deleteFlow x y (PetriLike ns) = PetriLike + . M.adjust (updateCapacityNode (M.delete y)) x + $ ns + + deleteNode x ns = PetriLike + . adjustAll (updateCapacityNode (M.delete x)) (Just $ M.keys $ allNodes ns) + . M.delete x + . allNodes + $ ns + + alterFlow x f y = PetriLike + . M.adjust (updateCapacityNode (M.insert y f)) x + . allNodes + + alterNode x mt = PetriLike . M.alter alterNode' x . allNodes + where + alterNode' = Just . fromMaybe + (maybe CapacityTransition (CapacityPlace undefined) mt M.empty) + + outFlow x = maybe M.empty flowOutCN . M.lookup x . allNodes + + mapNet = mapPetriLike + traverseNet = traversePetriLike + +flowOutCN :: CapacityNode a -> Map a Int +flowOutCN CapacityPlace {flowOut} = flowOut +flowOutCN CapacityTransition {flowOut} = flowOut + +updateCapacityNode :: (Map a Int -> Map b Int) -> CapacityNode a -> CapacityNode b +updateCapacityNode h (CapacityPlace c t o) = CapacityPlace c t (h o) +updateCapacityNode h (CapacityTransition o) = CapacityTransition (h o) + {-| A 'Functor' like 'fmap' on 'PetriLike'. @@ -661,22 +776,26 @@ petriLikeToPetri p = do = throwM RelatedNodesOfTransitionsContainTransitions | any (`M.member` ps) (allRelatedNodes ps) = throwM RelatedNodesOfPlacesContainPlaces - | any (any (<= 0) . flowIn) ts + | any (any (<= 0) . flowInN) ts = throwM FlowToATransitionIsZeroOrLess | any (any (<= 0) . flowOutN) ts = throwM FlowFromATransitionIsZeroOrLess | otherwise = pure () - toChangeTuple n = (toFlowList flowIn n, toFlowList flowOutN n) + toChangeTuple n = (toFlowList flowInN n, toFlowList flowOutN n) toFlowList f n = M.foldrWithKey (\k _ xs -> fromMaybe 0 (M.lookup k $ f n) : xs) [] ps - relatedNodes n = M.keysSet (flowIn n) `S.union` M.keysSet (flowOutN n) + relatedNodes n = M.keysSet (flowInN n) `S.union` M.keysSet (flowOutN n) allRelatedNodes = foldr (S.union . relatedNodes) S.empty +flowInN :: Node a -> Map a Int +flowInN (PlaceNode _ flowIn _ ) = flowIn +flowInN (TransitionNode flowIn _) = flowIn + type Marking = [Int] type Transition = (Marking,Marking) @@ -743,7 +862,7 @@ data GraphConfig = GraphConfig { defaultGraphConfig :: GraphConfig defaultGraphConfig = GraphConfig { - graphLayouts = [Dot, Neato, TwoPi, Circo, Fdp, Sfdp, Osage, Patchwork], + graphLayouts = [Dot, Neato, TwoPi, Circo, Fdp, Sfdp, Osage], hidePlaceNames = False, hideTransitionNames = False, hideWeight1 = True @@ -876,7 +995,7 @@ data FindConcurrencyConfig = FindConcurrencyConfig defaultFindConcurrencyConfig :: FindConcurrencyConfig defaultFindConcurrencyConfig = FindConcurrencyConfig { basicConfig = defaultBasicConfig { atLeastActive = 3 } - , advConfig = defaultAdvConfig{ presenceOfSourceTransitions = Just False } + , advConfig = defaultAdvConfig { presenceOfSourceTransitions = Just False } , changeConfig = defaultChangeConfig , graphConfig = defaultGraphConfig { hidePlaceNames = True } , printSolution = True @@ -904,10 +1023,100 @@ defaultPickConcurrencyConfig = PickConcurrencyConfig , printSolution = True , prohibitSourceTransitions = False , useDifferentGraphLayouts = False + , alloyConfig = defaultAlloyConfig { timeout = Just 60000000 } + , extraText = NoExtraText + } + +data PickMistakeConfig = PickMistakeConfig + { basicConfig :: BasicConfig + , changeConfig :: ChangeConfig + , mistakeConfig :: MistakeConfig + , graphConfig :: GraphConfig + , printSolution :: Bool + , useDifferentGraphLayouts :: Bool + , alloyConfig :: AlloyConfig + , extraText :: ExtraText + } + deriving (Generic, Read, Reader, Show, ToDoc) + +defaultPickMistakeConfig :: PickMistakeConfig +defaultPickMistakeConfig = PickMistakeConfig + { basicConfig = defaultBasicConfig { atLeastActive = 0 } + , changeConfig = defaultChangeConfig + , mistakeConfig = defaultMistakeConfig + , graphConfig = defaultGraphConfig { hidePlaceNames = True, hideTransitionNames = True } + , printSolution = False + , useDifferentGraphLayouts = False , alloyConfig = defaultAlloyConfig , extraText = NoExtraText } +data MistakeConfig = MistakeConfig + { canHaveNegativeWeight :: Bool + , canHaveTransitionToTransition :: Bool + , canHavePlaceToPlace :: Bool + } + deriving (Generic, Read, Reader, Show, ToDoc) + +defaultMistakeConfig :: MistakeConfig +defaultMistakeConfig = MistakeConfig + { canHaveNegativeWeight = True + , canHaveTransitionToTransition = True + , canHavePlaceToPlace = True + } + +data FindActivatedTransitionsConfig = FindActivatedTransitionsConfig + { basicConfig :: BasicConfig + , advConfig :: AdvConfig + , changeConfig :: ChangeConfig + , atMostActive :: Maybe Int + , graphConfig :: GraphConfig + , printSolution :: Bool + , alloyConfig :: AlloyConfig + , extraText :: ExtraText + } + deriving (Generic, Read, Reader, Show, ToDoc) + +defaultFindActivatedTransitionsConfig :: FindActivatedTransitionsConfig +defaultFindActivatedTransitionsConfig = FindActivatedTransitionsConfig + { basicConfig = defaultBasicConfig { atLeastActive = 1 } + , advConfig = defaultAdvConfig + , changeConfig = defaultChangeConfig + , atMostActive = Nothing + , graphConfig = defaultGraphConfig + , printSolution = False + , alloyConfig = defaultAlloyConfig + , extraText = NoExtraText + } + +data CapacityConfig = CapacityConfig + { basicConfig :: BasicConfig + , advConfig :: AdvConfig + , maxCapacity :: Int + , newArrowsWithComplement :: (Int, Int) + , oneMinCapacity :: Int + , distractors :: (Int, Int) + , atMostActive :: Maybe Int + , graphConfig :: GraphConfig + , printSolution :: Bool + , alloyConfig :: AlloyConfig + } + deriving (Generic, Read, Reader, Show, ToDoc) + +defaultCapacityConfig :: CapacityConfig +defaultCapacityConfig = CapacityConfig + { basicConfig = defaultBasicConfig { places = 2, transitions = 2, atLeastActive = 1, maxTokensPerPlace = 4, tokensOverall = (2, 8)} + , advConfig = defaultAdvConfig { presenceOfSinkTransitions = Just True } + , maxCapacity = 4 + , newArrowsWithComplement = (2, 6) + , oneMinCapacity = 2 + , atMostActive = Nothing + , distractors = (0, 1) + , graphConfig = defaultGraphConfig { hidePlaceNames = False, hideTransitionNames = False } + , printSolution = True + , alloyConfig = defaultAlloyConfig + } + data DrawSettings = DrawSettings { withPlaceNames :: Bool, withSvgHighlighting :: Bool, @@ -953,8 +1162,21 @@ transitionPairShow (t1, t2) = let (first, second) = if t1 <= t2 then (t1, t2) else (t2, t1) in bimap ShowTransition ShowTransition (first, second) -checkBasicConfig :: BasicConfig -> Maybe String -checkBasicConfig BasicConfig{ +transitionListShow :: [Petri.Transition] -> [ShowTransition] +transitionListShow = map ShowTransition + +petriScopeBitWidth :: [Int] -> Int +petriScopeBitWidth values = + floor + (2 + ((logBase :: Double -> Double -> Double) 2.0 . fromIntegral) + (maximum values) + ) + +basicConfigBitWidthInput :: BasicConfig -> [Int] +basicConfigBitWidthInput BasicConfig {places, transitions, flowOverall, tokensOverall} = [places, transitions, snd flowOverall, snd tokensOverall] + +checkBasicConfig :: [Int] -> BasicConfig -> Maybe String +checkBasicConfig values basicC@BasicConfig{ atLeastActive, flowOverall, maxFlowPerEdge, @@ -997,9 +1219,21 @@ checkBasicConfig BasicConfig{ = Just "The maximum 'flowOverall' is set unreasonably high, given the other parameters." | transitions + places > 1 + fst flowOverall = Just "The number of transitions and places exceeds the minimum 'flowOverall' too much to create a connected net." + | Just maxValue <- maxBitWidth, petriScopeBitWidth (basicConfigBitWidthInput basicC ++ values) > maxValue + = Just ("'places', 'transitions', " ++ addStrings values ++ "and the maximum 'flowOverall' and 'tokensOverall' should not be set too high.") | otherwise = Nothing +addStrings :: [Int] -> String +addStrings xs = intercalate ", " (map (\x -> "'" ++ show x ++ "'") xs) + +checkActivatedSourceConfig :: BasicConfig -> AdvConfig -> Maybe String +checkActivatedSourceConfig BasicConfig{ atLeastActive } AdvConfig{ presenceOfSourceTransitions } + | presenceOfSourceTransitions == Just True && atLeastActive == 0 + = Just "atLeastActive has to be at least 1 for source transitions to exist." + | otherwise + = Nothing + checkChangeConfig :: BasicConfig -> ChangeConfig -> Maybe String checkChangeConfig BasicConfig { @@ -1071,3 +1305,10 @@ checkPetriNodeCount countOfPetriNodesBounds petri = let count = M.size $ nodes petri in fst countOfPetriNodesBounds <= count && maybe True (count <=) (snd countOfPetriNodesBounds) + +prohibitPatchworkRenderer :: GraphConfig -> Maybe String +prohibitPatchworkRenderer gc + | Patchwork `elem` graphLayouts gc + = Just "Do not use 'Patchwork' as a GraphViz Renderer as it does not work properly." + | otherwise + = Nothing diff --git a/stack-apps.yaml b/stack-apps.yaml index dc00a7469..42b72dfa8 100644 --- a/stack-apps.yaml +++ b/stack-apps.yaml @@ -10,6 +10,8 @@ flags: quick-testing: true autotool-capabilities: alloy-use-sat4j: false +ghc-options: + autotool-capabilities: -DMAX_BIT_WIDTH=7 extra-deps: - git: https://github.com/fmidue/output-blocks.git commit: d67590cb2e1a72ed72437a8cfe2972b680405569 diff --git a/stack-examples.yaml b/stack-examples.yaml index 464c90169..a075f6e45 100644 --- a/stack-examples.yaml +++ b/stack-examples.yaml @@ -8,6 +8,8 @@ flags: quick-testing: true autotool-capabilities: alloy-use-sat4j: false +ghc-options: + autotool-capabilities: -DMAX_BIT_WIDTH=7 extra-deps: - git: https://github.com/fmidue/output-blocks.git commit: d67590cb2e1a72ed72437a8cfe2972b680405569 diff --git a/stack.yaml b/stack.yaml index ed05dcb4a..78f378c7e 100644 --- a/stack.yaml +++ b/stack.yaml @@ -7,6 +7,8 @@ flags: quick-testing: true autotool-capabilities: alloy-use-sat4j: false +ghc-options: + autotool-capabilities: -DMAX_BIT_WIDTH=7 extra-deps: - git: https://github.com/fmidue/output-blocks.git commit: d67590cb2e1a72ed72437a8cfe2972b680405569 diff --git a/test/Modelling/PetriNet/AlloySpec.hs b/test/Modelling/PetriNet/AlloySpec.hs index 2c2896b2d..322df0919 100644 --- a/test/Modelling/PetriNet/AlloySpec.hs +++ b/test/Modelling/PetriNet/AlloySpec.hs @@ -1,8 +1,9 @@ module Modelling.PetriNet.AlloySpec where -import Modelling.PetriNet.Alloy import Modelling.PetriNet.Types ( + basicConfigBitWidthInput, defaultBasicConfig, + petriScopeBitWidth, ) import Test.Hspec @@ -12,8 +13,4 @@ spec = do describe "petriScopeBitWidth" $ context "computes the needed bit width for generating Petri nets with Alloy" $ it "taking some values out of the user's input" $ - petriScopeBitWidth defaultBasicConfig `shouldSatisfy` (< 7) - describe "petriScopeMaxSeq" $ - context "computes the maximal needed space for generating Petri nets with Alloy" $ - it "taking some values out of the user's input" $ - petriScopeMaxSeq defaultBasicConfig `shouldSatisfy` (< 10) + petriScopeBitWidth (basicConfigBitWidthInput defaultBasicConfig) `shouldSatisfy` (< 7) diff --git a/test/Modelling/PetriNet/CapacitySpec.hs b/test/Modelling/PetriNet/CapacitySpec.hs new file mode 100644 index 000000000..5861606ea --- /dev/null +++ b/test/Modelling/PetriNet/CapacitySpec.hs @@ -0,0 +1,101 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DuplicateRecordFields #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE PartialTypeSignatures #-} +{-# OPTIONS_GHC -fno-warn-partial-type-signatures #-} + +module Modelling.PetriNet.CapacitySpec where + +import qualified Modelling.PetriNet.Types as Find ( + CapacityConfig (alloyConfig), + ) + +import Modelling.PetriNet.Capacity ( + checkCapacityConfigs, + checkCapacityConfig, + combinedCapacityInstance, + findCapacityInstance, + petriNetFindCapacity, + ) +import Modelling.PetriNet.Types ( + AdvConfig (AdvConfig), + BasicConfig (..), + CapacityConfig (CapacityConfig), + CapacityNode (..), + PetriLike (..), + PetriChangeList (..), + SimplePetriLike, + defaultCapacityConfig, + ) + +import Modelling.PetriNet.TestCommon ( + alloyTestConfig, + checkConfigs, + defaultConfigTaskGeneration, + firstInstanceConfig, + testTaskGeneration, + validAdvConfigs, + validConfigsForFind, + validGraphConfig, + ) +import Settings (configDepth, nightly) +import Control.Monad.Trans (lift) +import Data.Maybe (fromMaybe, isNothing) + +import Test.Hspec + +spec :: Spec +spec = do + describe "defaultCapacityConfig" $ + checkConfigs checkCapacityConfigs [defaultCapacityConfig] + describe "validFindCapacityConfigs" $ + checkConfigs checkCapacityConfigs findConfigs' + describe "combinedCapacity, part 1" $ + defaultConfigTaskGeneration + (combinedCapacityInstance defaultCapacityConfig { + Find.alloyConfig = firstInstanceConfig + } 0) + 0 + $ checkCapacityInstance @(SimplePetriLike _) + nightly $ + describe "combinedCapacity, part 2" $ + testCapacityConfig findConfigs + where + findConfigs' = validFindCapacityConfigs + validFinds + (AdvConfig Nothing Nothing Nothing) + findConfigs = validAdvConfigs >>= validFindCapacityConfigs validFinds + validFinds = validConfigsForFind 0 configDepth + +checkCapacityInstance :: (PetriLike CapacityNode String, a, PetriChangeList String, [(String, String)]) -> Bool +checkCapacityInstance (_, _, change, _) = isValidCapacity change + +testCapacityConfig :: [CapacityConfig] -> Spec +testCapacityConfig = testTaskGeneration + petriNetFindCapacity + (lift . findCapacityInstance) + $ checkCapacityInstance @(SimplePetriLike _) + +validFindCapacityConfigs :: [(BasicConfig, _)] -> AdvConfig -> [CapacityConfig] +validFindCapacityConfigs cs advancedConfig = do + (bc, _) <- cs + (maxCapacity, newArrows, oneMin, distractors, atMost) <- validCapacityConfig bc + return $ CapacityConfig bc advancedConfig maxCapacity newArrows oneMin distractors atMost validGraphConfig False alloyTestConfig + +validCapacityConfig :: BasicConfig -> [(Int, (Int, Int), Int, (Int, Int), Maybe Int)] +validCapacityConfig bc@BasicConfig{ places, transitions, maxTokensPerPlace, atLeastActive } = + filter (\(maxCap, arrows, oneMinCap, distract, most) -> isNothing (checkCapacityConfig bc maxCap arrows oneMinCap distract most)) $ do + maxCapacity <- [maxTokensPerPlace .. 5] + newArrows <- [(a, b) | a <- [places .. 2 * transitions * places], b <- [a .. 2 * transitions * places]] + oneMin <- [1 .. maxCapacity] + atMost <- Nothing : [Just n | n <- [atLeastActive .. transitions - 1]] + distractors <- [(x, y) | x <- [0 .. transitions - fromMaybe transitions atMost], y <- [x .. transitions - atLeastActive]] + return (maxCapacity, newArrows, oneMin, distractors, atMost) + +isValidCapacity :: PetriChangeList String -> Bool +isValidCapacity c@(ChangeList {tokenChanges = ts, flowChanges = fs}) + | any (\(_, token) -> token < 0) ts = error $ show c + | any (\(source, target, _) -> source == target) fs = error $ show c + | any (\(_, _, flow) -> flow <= 0) fs = error $ show c + | otherwise = True diff --git a/test/Modelling/PetriNet/DiagramSpec.hs b/test/Modelling/PetriNet/DiagramSpec.hs index 465290455..c29562f49 100644 --- a/test/Modelling/PetriNet/DiagramSpec.hs +++ b/test/Modelling/PetriNet/DiagramSpec.hs @@ -13,7 +13,7 @@ import Modelling.PetriNet.Types ( defaultAdvConfig, defaultBasicConfig, ) -import Modelling.PetriNet.Parser (parseNet) +import Modelling.PetriNet.Parser (parseNet, singleSig) import Data.GraphViz.Attributes.Complete (GraphvizCommand (TwoPi)) import Diagrams.Backend.SVG (renderSVG) @@ -29,7 +29,7 @@ spec = do (inst:_) <- getInstances (Just 1) (petriNetRnd defaultBasicConfig defaultAdvConfig) - pl <- parseNet "flow" "tokens" inst + pl <- parseNet (singleSig "this" "Nodes" "") "flow" "tokens" inst dia <- drawNet (mapNet show (pl :: SimplePetriLike Object)) DrawSettings { withPlaceNames = True, withSvgHighlighting = True, diff --git a/test/Modelling/PetriNet/FindActivatedTransitionsSpec.hs b/test/Modelling/PetriNet/FindActivatedTransitionsSpec.hs new file mode 100644 index 000000000..bec3be71b --- /dev/null +++ b/test/Modelling/PetriNet/FindActivatedTransitionsSpec.hs @@ -0,0 +1,104 @@ +{-# LANGUAGE DuplicateRecordFields #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE TypeApplications #-} + +module Modelling.PetriNet.FindActivatedTransitionsSpec where + +import qualified Modelling.PetriNet.Types as Find ( + FindActivatedTransitionsConfig (alloyConfig), + ) + +import Modelling.PetriNet.FindActivatedTransitions ( + checkActivatedTransitionsConfig, + checkFindActivatedTransitionsConfig, + findActivatedTransitions, + parseActivatedTransitions, + petriNetFindActivatedTransitions, + ) + +import Modelling.PetriNet.Find ( + findTaskInstance, + ) +import Modelling.PetriNet.Types ( + ActivatedTransitions (..), + AdvConfig (AdvConfig), + BasicConfig (..), + ChangeConfig, + FindActivatedTransitionsConfig (FindActivatedTransitionsConfig), + SimplePetriLike, + defaultFindActivatedTransitionsConfig, + ) + +import Modelling.PetriNet.TestCommon ( + alloyTestConfig, + checkConfigs, + defaultConfigTaskGeneration, + firstInstanceConfig, + testTaskGeneration, + validAdvConfigs, + validConfigsForFind, + validGraphConfig, + ) +import Settings (configDepth) + +import Control.Lens.Lens ((??)) +import Control.OutputCapable.Blocks (ExtraText (..)) +import Data.Char (isDigit) +import Data.List (nub) +import Data.Maybe (isNothing) +import Test.Hspec + +spec :: Spec +spec = do + describe "defaultFindActivatedTransitionsConfig" $ + checkConfigs checkFindActivatedTransitionsConfig [defaultFindActivatedTransitionsConfig] + describe "validFindActivatedTransitionsConfigs" $ + checkConfigs checkFindActivatedTransitionsConfig findConfigs' + describe "findActivatedTransitions" $ do + defaultConfigTaskGeneration + (findActivatedTransitions defaultFindActivatedTransitionsConfig { + Find.alloyConfig = firstInstanceConfig + } 0) + 0 + $ checkFindActivatedTransitionsInstance @(SimplePetriLike _) + testFindActivatedTransitionsConfig findConfigs + where + findConfigs' = validFindActivatedTransitionsConfigs + validFinds + (AdvConfig Nothing Nothing Nothing) + findConfigs = validAdvConfigs >>= validFindActivatedTransitionsConfigs validFinds + validFinds = validConfigsForFind 0 configDepth + +checkFindActivatedTransitionsInstance :: (a, ActivatedTransitions String) -> Bool +checkFindActivatedTransitionsInstance = isValidActivatedTransitions . snd + +testFindActivatedTransitionsConfig :: [FindActivatedTransitionsConfig] -> Spec +testFindActivatedTransitionsConfig = testTaskGeneration + petriNetFindActivatedTransitions + (findTaskInstance parseActivatedTransitions) + $ checkFindActivatedTransitionsInstance @(SimplePetriLike _) + +validFindActivatedTransitionsConfigs + :: [(BasicConfig, ChangeConfig)] + -> AdvConfig + -> [FindActivatedTransitionsConfig] +validFindActivatedTransitionsConfigs cs advancedConfig = do + (bc, ch) <- cs + FindActivatedTransitionsConfig bc advancedConfig ch + <$> validActivatedTransitionsConfigs bc + <*> pure validGraphConfig + <*> pure False + <*> pure alloyTestConfig + ?? NoExtraText + +validActivatedTransitionsConfigs :: BasicConfig -> [Maybe Int] +validActivatedTransitionsConfigs bc@BasicConfig{ transitions } = filter (isNothing . checkActivatedTransitionsConfig bc) $ + Nothing : [Just n | n <- [0 .. transitions - 1]] + +isValidActivatedTransitions :: ActivatedTransitions String -> Bool +isValidActivatedTransitions a@(ActivatedTransitions ts) + | length ts == length (nub ts) && all isNumber ts = True + | otherwise = error $ show a + where + isNumber ('t':x) = all isDigit x + isNumber _ = False diff --git a/test/Modelling/PetriNet/PickMistakeSpec.hs b/test/Modelling/PetriNet/PickMistakeSpec.hs new file mode 100644 index 000000000..cd05d8809 --- /dev/null +++ b/test/Modelling/PetriNet/PickMistakeSpec.hs @@ -0,0 +1,93 @@ +{-# LANGUAGE DuplicateRecordFields #-} +{-# LANGUAGE TypeApplications #-} +module Modelling.PetriNet.PickMistakeSpec where + +import qualified Modelling.PetriNet.Types as Pick ( + PickMistakeConfig (..), + ) + +import Modelling.PetriNet.PickMistake ( + checkMistakeConfig, + checkPickMistakeConfig, + petriNetPickMistake, + pickMistake, + ) + +import Modelling.PetriNet.Pick ( + pickTaskInstance, + ) +import Modelling.PetriNet.Types ( + BasicConfig, + ChangeConfig, + MistakeConfig (..), + PickMistakeConfig (..), + SimplePetriLike, + defaultPickMistakeConfig, + ) + +import Modelling.PetriNet.TestCommon ( + alloyTestConfig, + checkConfigs, + defaultConfigTaskGeneration, + firstInstanceConfig, + testTaskGeneration, + validConfigsForPick, + validGraphConfig, + ) +import Settings (configDepth) + +import Control.Lens.Lens ((??)) +import Control.OutputCapable.Blocks (ExtraText (..)) +import Data.Functor.Const (Const(..)) +import Data.Maybe (isNothing) +import Test.Hspec + +spec :: Spec +spec = do + describe "defaultPickMistakeConfig" $ + checkConfigs checkPickMistakeConfig [defaultPickMistakeConfig] + describe "validPickMistakeConfigs" $ + checkConfigs checkPickMistakeConfig pickConfigs + describe "pickMistake" $ do + defaultConfigTaskGeneration + (pickMistake defaultPickMistakeConfig { + Pick.alloyConfig = firstInstanceConfig + } 0) + 0 + $ checkPickMistakeInstance @(SimplePetriLike _) + testPickMistakeConfig pickConfigs + where + pickConfigs = validPickMistakeConfigs validPicks + validPicks = validConfigsForPick 0 configDepth + +checkPickMistakeInstance :: [(a, Maybe (Const () String))] -> Bool +checkPickMistakeInstance = f . fmap snd + where + f [Just (Const ()), Nothing] = True + f _ = False + +testPickMistakeConfig :: [PickMistakeConfig] -> Spec +testPickMistakeConfig = testTaskGeneration + petriNetPickMistake + (pickTaskInstance (const (return (Const ())))) + $ checkPickMistakeInstance @(SimplePetriLike _) + +validMistakeConfigs :: BasicConfig -> ChangeConfig -> [MistakeConfig] +validMistakeConfigs bc ch = filter (isNothing . checkMistakeConfig bc ch) $ do + negative <- [False, True] + transitionToTransition <- [False, True] + placeToPlace <- [False, True] + [MistakeConfig negative transitionToTransition placeToPlace] + +validPickMistakeConfigs + :: [(BasicConfig, ChangeConfig)] + -> [PickMistakeConfig] +validPickMistakeConfigs cs = do + (bc, ch) <- cs + PickMistakeConfig bc ch + <$> validMistakeConfigs bc ch + <*> pure validGraphConfig + <*> pure False + ?? False + ?? alloyTestConfig + ?? NoExtraText diff --git a/test/Modelling/PetriNet/TypesSpec.hs b/test/Modelling/PetriNet/TypesSpec.hs index 1946c952b..15279c18a 100644 --- a/test/Modelling/PetriNet/TypesSpec.hs +++ b/test/Modelling/PetriNet/TypesSpec.hs @@ -27,10 +27,10 @@ spec :: Spec spec = do describe "checkBasicConfig" $ do it "checks if the basic Input is in given boundaries" $ - checkBasicConfig defaultBasicConfig `shouldBe` Nothing + checkBasicConfig [] defaultBasicConfig `shouldBe` Nothing context "when provided with Input out of the constraints" $ it "it returns a String with necessary changes" $ - checkBasicConfig defaultBasicConfig{places = 0} + checkBasicConfig [] defaultBasicConfig{places = 0} `shouldSatisfy` isJust describe "checkChangeConfig" $ do it "checks if the input for Changes is in given boundaries" $