Marcin Szpyrka - wiki - alvis
https://home.agh.edu.pl/~mszpyrka/
2026-05-02T03:52:05+00:00Marcin Szpyrka - wiki
https://home.agh.edu.pl/~mszpyrka/
https://home.agh.edu.pl/~mszpyrka/lib/exe/fetch.php?media=wiki:dokuwiki.svgtext/html2026-05-01T11:00:44+00:00Anonymous (anonymous@undisclosed.example.com)active2
https://home.agh.edu.pl/~mszpyrka/doku.php?id=alvis:active2&rev=1777633244&do=diff
Communication between active agents
agent A {
loop { -- 1
out a; -- 2
}
}
agent B {
loop { -- 1
in b; -- 2
}
}text/html2026-05-01T11:01:10+00:00Anonymous (anonymous@undisclosed.example.com)active2passive1
https://home.agh.edu.pl/~mszpyrka/doku.php?id=alvis:active2passive1&rev=1777633270&do=diff
Communication with a passive agent
agent A, C {
x :: Int = 5;
out q x; -- 1
}
agent B {
x :: Int = 0;
proc p1 {
in p1 x; -- 1
exit; -- 2
}
proc p2 {
in p2 x; -- 3
exit; -- 4
}
}text/html2026-05-01T10:52:47+00:00Anonymous (anonymous@undisclosed.example.com)compiler
https://home.agh.edu.pl/~mszpyrka/doku.php?id=alvis:compiler&rev=1777632767&do=diff
Usage of compiler
Basic usage of the compiler is to produce an intermediate Haskell representation of an Alvis model.
The intermediate representation may be used to generate the Label Transition System (LTS graph) for the given model.
The Alvis compiler requires a Haskell compiler to be installed.text/html2026-05-01T10:52:05+00:00Anonymous (anonymous@undisclosed.example.com)editor
https://home.agh.edu.pl/~mszpyrka/doku.php?id=alvis:editor&rev=1777632725&do=diff
Getting Started
This section gives you an overview of ALVIS, including installation, work area, file format to store Alvis model and license.
Installing ALVIS
A Java JRE 1.7 or higher required. ALVIS runs successfully on the most recent systems with Java installed on it. If your computer does not meet these requirements, you may not be able to use ALVIS.text/html2026-05-01T11:01:29+00:00Anonymous (anonymous@undisclosed.example.com)sbrexample
https://home.agh.edu.pl/~mszpyrka/doku.php?id=alvis:sbrexample&rev=1777633289&do=diff
Example: Sender-Buffer-Receiver system
Agent S (sender) puts sequentially valueless signals to the buffer (agent B) and agent R (receiver) gets such signals from the buffer. Agent B offers two procedures (services, ports) to connected agents.
agent S {
loop { -- 1 comments contain steps numbers
out put; -- 2
}
}
agent B {
i :: Int = 0;
proc (i == 0) put {
in put; -- 1
i = 1; -- 2
exit; -- 3
}
…text/html2026-05-01T11:02:55+00:00Anonymous (anonymous@undisclosed.example.com)start
https://home.agh.edu.pl/~mszpyrka/doku.php?id=alvis:start&rev=1777633375&do=diff
Alvis Team
* Prof. Marcin Szpyrka
* Piotr Matyasik, PhD
* Michał Wypych, PhD
* Jerzy Biernacki, PhD
* Łukasz Podolski, MSc
Documentation
* [Alvis Manual v. 0.13]
* Getting Started with Alvis Editor
* Getting Started with Alvis Compiler
Download
*
* [Alvis Compiler v. 0.4.3.33]
Examples
* Communication between active agents
* Communication with a passive agent
* Sender-Buffer-Receiver example
* [ Test models] The archive contains selected Alvis test models: