Portal:Tutorials - Revision history

Signe at 12:57, 17 May 2022

2022-05-17T12:57:01Z

@@ Line 1: / Line 1: @@
-;Verification Tools & Processes Tutorials
+== Verification-Focused Tools & Processes Tutorials ==
-;Autonomy Tools & Processes Tutorials
+== Autonomy-Focused Tools & Processes Tutorials ==
 * Andre Platzer [https://keymaerax.org/Xtutorial.html Tutorial on how to use Keymaera-X]

2022-05-17T12:04:59Z

← Older revision		Revision as of 12:04, 17 May 2022
Line 40:		Line 40:
	End.		End.

			;KeymaeraX DrivelineDynamics
	ArchiveEntry "DrivelineDynamics"		ArchiveEntry "DrivelineDynamics"
	Definitions		Definitions
Line 51:		Line 52:
	Real K2 = 57.1911;		Real K2 = 57.1911;
	Real K3 = -12.9458;		Real K3 = -12.9458;
			HP ctrl ::= {u := -(K1Weng + K2Wwheel + K3*phi);};
	HP ctrl ::= {u := -(K1Weng + K2Wwheel + K3*phi);};

	HP driveline ::= {{		HP driveline ::= {{
	Weng' = (1/Jf)(u - (1/r)(csphi + ds((Weng/r)-Wwheel))),		Weng' = (1/Jf)(u - (1/r)(csphi + ds((Weng/r)-Wwheel))),

2022-05-17T12:04:00Z

2022-05-17T12:03:44Z

← Older revision		Revision as of 12:03, 17 May 2022
Line 42:		Line 42:

	ArchiveEntry "DrivelineDynamics"		ArchiveEntry "DrivelineDynamics"

	Definitions		Definitions
	Real Jf = 0.625;		Real Jf = 0.625;
Line 63:		Line 62:

	End.		End.

	ProgramVariables		ProgramVariables
	Real Weng; /engine speed/		Real Weng; /engine speed/
Line 70:		Line 68:
	Real u; /control input/		Real u; /control input/
	End.		End.

	Problem		Problem
	Weng > 0 & Wwheel > 0 & phi > 0 -> [{ctrl; driveline;}*] Weng >= 0 & Wwheel > 0 & phi = 0		Weng > 0 & Wwheel > 0 & phi > 0 -> [{ctrl; driveline;}*] Weng >= 0 & Wwheel > 0 & phi = 0
	End.		End.
	End.		End.

2022-05-17T12:03:09Z

← Older revision		Revision as of 12:03, 17 May 2022
Line 10:		Line 10:

	*		*
			;KeyMaeraX - Garage Door

			ArchiveEntry "Garage Door"
			Definitions
			Real m = 50;
			Real k = 600;
			Real K = 0.6;
			Real R = 0.005;
			Real J = 0.02;
			Real Kp = 240;

			Real error(Real ref, Real theta) = (ref - theta);

			HP ctrl ::= {u := Kp*error;};

			HP motion ::= {{
			theta' = thetadt,
			thetadt' = (KR^2)/(J+mR^2)theta + (KR)/(J+mR^2)u
			& theta >=0}};

			End.
			ProgramVariables
			Real theta; /position/
			Real thetadt; /velocity/
			Real u; /control input/
			End.
			Problem
			theta > 0 -> [{ctrl; motion;}*] theta >= 0
			End.
			End.

			ArchiveEntry "DrivelineDynamics"

			Definitions
			Real Jf = 0.625;
			Real Jc = 6250;
			Real cs = 65000;
			Real ds = 1000;
			Real Tload = 7000;
			Real r = 12.5;
			Real K1 = 5.4567;
			Real K2 = 57.1911;
			Real K3 = -12.9458;

			HP ctrl ::= {u := -(K1Weng + K2Wwheel + K3*phi);};

			HP driveline ::= {{
			Weng' = (1/Jf)(u - (1/r)(csphi + ds((Weng/r)-Wwheel))),
			Wwheel' = (1/Jc)(csphi + ds*((Weng/r)-Wwheel)-Tload),
			phi' = (Weng/r) - Wwheel
			}};

			End.

			ProgramVariables
			Real Weng; /engine speed/
			Real Wwheel; /wheel speed/
			Real phi; /torsion/
			Real u; /control input/
			End.

			Problem
			Weng > 0 & Wwheel > 0 & phi > 0 -> [{ctrl; driveline;}*] Weng >= 0 & Wwheel > 0 & phi = 0
			End.
			End.

2022-05-03T12:24:26Z

← Older revision		Revision as of 12:24, 3 May 2022
Line 1:		Line 1:
	;Verification Tutorials		;Verification Tools & Processes Tutorials


	;Autonomy Tutorials		;Autonomy Tools & Processes Tutorials


	;Verification of Autonomous Systems Tutorials		;Verification of Autonomous Systems Tools & Processes Tutorials

	* Andre Platzer [https://keymaerax.org/Xtutorial.html Tutorial on how to use Keymaera-X]		* Andre Platzer [https://keymaerax.org/Xtutorial.html Tutorial on how to use Keymaera-X]

	*		*

2022-05-03T12:23:40Z

← Older revision		Revision as of 12:23, 3 May 2022
Line 1:		Line 1:
			;Verification Tutorials


			;Autonomy Tutorials


			;Verification of Autonomous Systems Tutorials

	* Andre Platzer [https://keymaerax.org/Xtutorial.html Tutorial on how to use Keymaera-X]		* Andre Platzer [https://keymaerax.org/Xtutorial.html Tutorial on how to use Keymaera-X]

	*		*

2022-04-05T12:41:37Z

Created page with "* Andre Platzer [https://keymaerax.org/Xtutorial.html Tutorial on how to use Keymaera-X] *"

New page

* Andre Platzer [https://keymaerax.org/Xtutorial.html Tutorial on how to use Keymaera-X]

*