diff --git a/ginger-cat-713.png b/ginger-cat-713.png new file mode 100644 index 0000000..beaf259 Binary files /dev/null and b/ginger-cat-713.png differ diff --git a/ginger-cat-718.png b/ginger-cat-718.png new file mode 100644 index 0000000..c8d9115 Binary files /dev/null and b/ginger-cat-718.png differ diff --git a/ginger-cat-746.png b/ginger-cat-746.png new file mode 100644 index 0000000..8f20451 Binary files /dev/null and b/ginger-cat-746.png differ diff --git a/index.html b/index.html new file mode 100644 index 0000000..6474dd3 --- /dev/null +++ b/index.html @@ -0,0 +1,155 @@ + + + + + BaaS: Bisimulation as a Service + + + + + + + + + + + +
+
+
+

BaaS

+

Bisimulation as a Service

+
+ +
+

Check behavioural equivalence of your models NOW! +

+
+ +
+
+

What we do as BaaS

+

We provide an online service for bisimulation checking. + Developers can now check behavioural equivalence with the touch of a button, increasing their productivity. + We support many types of bisimulation, including the latest up-to techniques. + +

You can register for a monthly subscription which allows you to check many models. + We provide a free plan with reduced functionality. +

+ +
+
+ +
+ +
+

What is a bisimulation?

+

Two systems are bisimilar if they match each other's moves. + In this sense, each of the systems cannot be distinguished from the other by an observer. + +

A bisimulation relation is a certificate of this equivalence. + Our service computes this certificate automatically for you. + This makes our service trustworthy and secure, as it does not only return a binary output. + +

If your system contains a bug, our service will not be able to produce this certificate. + Instead, it will return a counterexample, which can be used to resolve the bug. +

+ +
+

Efficient

+

Our algorithms are state-of-the art, using up-to techniques, making us the most efficient BaaS. + These up-to-techniques compress the bisimulation by using algebraic and coalgebraic properties of the system. + It allows the bisimulation algorithm to exit early and find bugs more quickly. + This is not only good for efficiency and throughput, it also shrinks the size of the certificate. +

+ +
+ +
+ +
+ +
+ +
+

Testimonials

+

Todo. + Lorem Ipsum is slechts een proeftekst uit het drukkerij- en zetterijwezen. Lorem Ipsum is de standaard proeftekst in deze bedrijfstak sinds de 16e eeuw, toen een onbekende drukker een zethaak met letters nam en ze door elkaar husselde om een font-catalogus te maken. Het heeft niet alleen vijf eeuwen overleefd maar is ook, vrijwel onveranderd, overgenomen in elektronische letterzetting. +

+
+ +
+

BaaS Plans

+ +

Get in touch to inquire about the pricing. + Below is a table of the different features we provide. + + +
You getFree PlanPremium Plan +
Maximal number of models per month109000 +
Maximal number of states per model501000000 +
Maximal number of transitions per model1009000000 + +
Features +
Standard (strong) bisimulation✓✓ +
Branching bisimulation✓ +
Bisimulation up-to transitive closure and congruence✓ +
Bisimulation up-to bisimulation✓ +
CEGAR & CEGIS API✓ +
O(m log n) algorithms✓ +
Big Data Types✓ + +
Models +
Deterministic Automata✓✓ +
Nondeterministic Automata✓ +
Weighted Automata✓✓ +
Weighted Tree Automata✓ +
Deterministic Register Automata✓ +
Quantum Software Product Line Systems✓ +
Labelled Transition Blockchain Coalgebras✓ +
+

+ +
+

Team

+

A CEO, some developers, some designers, etc. + All of them have a PhD in related fields, etc. + "Bisimulation evangelist." + +

+ +
+ Copyright 2020 JM + +
+
+ + + +
+ + \ No newline at end of file diff --git a/push.sh b/push.sh new file mode 100755 index 0000000..c1d0d64 --- /dev/null +++ b/push.sh @@ -0,0 +1,4 @@ +#!/bin/bash + +rsync -az --exclude '.git' --exclude "push.sh" ./ joshua@matser-moerman.eu:/var/www/bisimulation-online/ + diff --git a/style.css b/style.css new file mode 100644 index 0000000..debbe02 --- /dev/null +++ b/style.css @@ -0,0 +1,248 @@ +body { + margin: 0; + color: #034; + font-family: 'Open Sans', Frutiger, "Frutiger Linotype", Univers, Calibri, "Gill Sans", "Gill Sans MT", "Myriad Pro", Myriad, "DejaVu Sans Condensed", "Liberation Sans", "Nimbus Sans L", Tahoma, Geneva, "Helvetica Neue", Helvetica, Arial, sans-serif; + font-size: 13pt; + line-height: 1.25em; +} + +a { + color: #2babe1; +} +a:hover { + color: #034; +} + +header { + margin: 0 auto; + max-width: 1040px; + position: relative; + text-align: center; + top: 0; + width: 100%; + z-index: 1; +} +h1 { + font-family: 'Adelle W01 Bold', 'Arvo', Constantia, "Lucida Bright", Lucidabright, "Lucida Serif", Lucida, "DejaVu Serif", "Bitstream Vera Serif", "Liberation Serif", Georgia, serif; + font-size: 90px; + font-weight: 500; + + background-color: #fff; + color: #034; + display: inline-block; + min-height: 18px; + margin: 40px auto 0; + padding: 0 10px; + z-index: 2; +} +/* Creates horizontal line */ +h1:after { + background-color: #dd3b2a; + content: ''; + height: 12px; + left: 0; + margin-top: 2px; + position: absolute; + width: 100%; + z-index: -1; +} +h2 { + color: #dd3b2a; + font-size: 22px; + font-style: italic; + font-weight: 400; + + text-align: right; + max-width: 695px; + margin: -10px auto 0; + width: 100%; +} + +.summary { + position: relative; + max-width: 1040px; + margin: 20px auto; + z-index: 2; +} +.summary p { + color: #dd3b2a; + font-style: italic; + text-align: right; + max-width: 695px; + margin: 10px auto 0; +} + +.intro { + background: linear-gradient(to bottom, #ffffff 0%, #edf6ff 100%); + height: 450px; +} + +h3 { + color: #dd3b2a; + font-family: 'Adelle W01 Bold', 'Arvo', Constantia, "Lucida Bright", Lucidabright, "Lucida Serif", Lucida, "DejaVu Serif", "Bitstream Vera Serif", "Liberation Serif", Georgia, serif; + font-size: 40px; + font-weight: 500; + line-height: 1em; +} + +.main { + background-color: rgba(255, 255, 255, 0.9); + border-top: 5px solid #dd3b2a; + border-bottom: 5px solid #2babe1; + position: relative; + width: 100%; + z-index: 3; +} + +.main p, .main h3, .main .middle { + max-width: 495px; +} + +.middle { + margin: 25px auto 40px auto; +} + +.solide { + background: #edf6ff; + border-top: 5px solid #cce4fb; + border-bottom: 5px solid #cce4fb; + margin: 25px 0; + + display: grid; + grid-template-columns: auto auto; + grid-gap: 10px; + padding: 0 10%; + align-items: center; +} + +.solide > div { + padding: 20px 0; + max-width: 495px; + margin-left:auto; + margin-right:auto; +} + +.solide .cat { + max-height: 250px; +} + +table { + border-collapse: collapse; +} + +table th { + padding: 15px; +} + +table td { + text-align: center; + max-width: 200px; + padding: 10px; +} + +.rowheader { + border-bottom: 2px solid #dd3b2a; + margin-bottom: 15px; +} + +/* star */ +@keyframes spin { + from { transform: rotate(0deg); } + to { transform: rotate(360deg); } +} +aside:before { + animation: spin 37s infinite linear; + /*background: url('../images/starburst.png') center top no-repeat;*/ + background: url('data:image/svg+xml;base64, PD94bWwgdmVyc2lvbj0iMS4wIiBlbmNvZGluZz0idXRmLTgiPz4NCjwhLS0gR2VuZXJhdG9yOiBBZG9iZSBJbGx1c3RyYXRvciAxNi4wLjQsIFNWRyBFeHBvcnQgUGx1Zy1JbiAuIFNWRyBWZXJzaW9uOiA2LjAwIEJ1aWxkIDApICAtLT4NCjwhRE9DVFlQRSBzdmcgUFVCTElDICItLy9XM0MvL0RURCBTVkcgMS4xLy9FTiIgImh0dHA6Ly93d3cudzMub3JnL0dyYXBoaWNzL1NWRy8xLjEvRFREL3N2ZzExLmR0ZCI+DQo8c3ZnIHZlcnNpb249IjEuMSIgaWQ9IkxheWVyXzEiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9yZy8yMDAwL3N2ZyIgeG1sbnM6eGxpbms9Imh0dHA6Ly93d3cudzMub3JnLzE5OTkveGxpbmsiIHg9IjBweCIgeT0iMHB4Ig0KCSB3aWR0aD0iOTIyLjU3NHB4IiBoZWlnaHQ9IjkyMS4wNzJweCIgdmlld0JveD0iMCAwIDkyMi41NzQgOTIxLjA3MiIgZW5hYmxlLWJhY2tncm91bmQ9Im5ldyAwIDAgOTIyLjU3NCA5MjEuMDcyIg0KCSB4bWw6c3BhY2U9InByZXNlcnZlIj4NCjxwb2x5Z29uIGZpbGw9IiNGRkZGRkYiIHBvaW50cz0iNzQ1Ljk0NSw4MjkuMDQyIDUxNS4wNzIsNTc3LjIyMiA1NzIuNjM1LDkxMy45NzIgNDY0LjE0Niw1OTAuMDIgMzc5Ljc2Myw5MjEuMDcyIDQxMi40MjEsNTgwLjk5OSANCgkyMDAuNjgyLDg0OS4xMDggMzY4LjgzNSw1NTEuNzIxIDY2LjM1Miw3MTAuNTI2IDM0MC45MjgsNTA3LjIzOSAwLDUyOS4yOTEgMzMzLjUyLDQ1NS4yNTYgMTMuMTAxLDMzNi43MzEgMzQ3Ljg5Niw0MDQuNzU2IA0KCTEwMy4zOTMsMTY2LjE1MyAzODEuNTc2LDM2NC40NzEgMjU1LjI1Nyw0Ny4wNDUgNDI4LjcyNCwzNDEuMzY2IDQ0Mi40MzYsMCA0ODEuMTk3LDMzOS40MzUgNjMyLjU2NiwzMy4xNTcgNTI5LjkyLDM1OS4wMTIgDQoJNzkyLjc3NiwxNDAuNzgyIDU2Ni40NjgsMzk2LjcxNCA4OTUuMzU2LDMwNC4yNjQgNTg0LjUxNCw0NDYuMDIxIDkyMi41NzQsNDk1LjMzNiA1ODAuOTUxLDQ5OC40MDkgODY5LjcyNCw2ODAuOTY0IA0KCTU1Ni4zODgsNTQ0LjgxNSAiLz4NCjwvc3ZnPg0K') center top no-repeat; + content: ''; + height: 921px; + left: 50%; + margin-left: -461.5px; + position: fixed; + top: 60px; + width: 923px; +} + +/* cats */ +@keyframes rise { + from { top: 100%; } + to { top: 165px; } +} +aside:after { + animation: rise 1.25s 1 ease; + background: url('ginger-cat-718.png') center no-repeat; + content: ''; + position: fixed; + z-index: 1; + left: 50%; + margin-left: -330px; + width: 660px; + height: 640px; + top: 165px; +} + +footer { + color: #fff; + padding: 20px; + background: #00374f; + font-size: 22px; + text-align: center; +} +footer a { + text-decoration: underline; +} +footer a:hover { + color: #fff; +} + +@media (max-width: 750px) { + .intro { + height: 320px; + } + aside:before { + top: 80px; + } + @keyframes rise-short { + from { top: 100%; } + to { top: 40px; } + } + aside:after { + background-size: 67%; + animation: rise-short 1.5s 1 ease; + top: 40px; + } + h1 { + font-size: 60px; + min-height: 50px; + margin-top: 35px; + } + .main footer { + font-size: 18px; + } + .middle { + /*width: 85%;*/ + } + .solide { + grid-template-columns: auto; + grid-gap: 0px; + } + .solide > div { + padding: 0px; + } + .solide .cat { + max-height: 140px; + padding: 10px; + } +} + +@media (max-width: 500px) { + body { + font-size: 15pt; + } + .solide { + padding: 5px; + } + .middle { + padding: 5px; + } +} \ No newline at end of file